全部 标题 作者
关键词 摘要

OALib Journal期刊
ISSN: 2333-9721
费用:99美元

查看量下载量

相关文章

更多...

基于等价类推理的几何自动推理网*

, PP. 617-628

Keywords: Rete算法,冗余推理,等价类推理,几何等价谓词,等词

Full-Text   Cite this paper   Add to My Lib

Abstract:

为了提高推理引擎的推理效率,将Rete算法和等价类推理技术整合到基于规则的几何自动推理系统中,构造一种新的推理引擎,即基于等价类推理的几何自动推理网.采用Lisp语言实现该推理引擎,并做了50多个非平凡几何定理的实验,实验结果表明该推理引擎具有更高的推理效率.

References

[1]  Wu W T. On the Decision Problem and the Mechanization ofTheorem Proving in Elementary Geometry. Scientia Sinica, 1978, 21: 157-179
[2]  Chou S C. Proving Elementary Geometry Theorems Using Wu’s Algorithm // Bledsoe W W, Loveland D W, eds. Automated Theorem Proving: After 25 Years. AMS Contemporary Mathematics Series, 1984, 29: 243-286
[3]  Chou S C, Gao X S, Zhang J Z. Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems. Singapore, Singapore: World Scientific, 1994
[4]  Chou S C, Gao X S, Zhang J Z. A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering. Journal of Automated Reasoning, 2000, 25(3): 219-246
[5]  Zhang Jinzhong, Gao Xiaoshan, Chou Xianqing. The Geometry Information Search System by Forward Reasoning. Chinese Journal of Computers, 1996, 19(10): 721-727 (in Chinese) (张景中,高小山,周咸青. 基于前推法的几何信息搜索系统. 计算机学报, 1996, 19(10): 721-727)
[6]  Chou S C, Gao X S. Automated Reasoning in Geometry // Robinson A, Voronkov A, eds. Handbook of Automated Reasoning. Amsterdam, Netherlands: Elsevier Science, 2001: 708-749
[7]  Gao Xiaoshan, Zhang Jinzhong, Chou Xianqing. Geometry Expert. Beijing, China: China Children’s Press, 1998 (in Chinese) (高小山,张景中,周咸青. 几何专家. 北京: 中国少年儿童出版社, 1998)
[8]  Li Chuanzhong, Zhang Jinzhong. Super Sketchpad (Version 2.0). Beijing, China: Beijing Normal University Press, 2004 (in Chinese) (李传中,张景中. 超级画板(V2.0). 北京: 北京师范大学出版社, 2004)
[9]  Gelernter H, Hansen J R, Loveland D W. Empirical Explorations of the Geometry Theorem-Proving Machine // Feigenbaum E, Feldman J, eds. Computers and Thought. New York, USA: McGraw-Hill, 1963: 153-163
[10]  Nevins A J. Plane Geometry Theorem Proving Using Forward Chaining. Artificial Intelligence, 1975, 6(1): 1-23
[11]  Forgy C L. Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem. Artificial Intelligence, 1982, 19(1): 17-37
[12]  Noboru M, Kurt V. GRAMY: A Geometry Theorem Prover Capable of Construction. Journal of Automated Reasoning, 2004, 32(1): 3-33

Full-Text

Contact Us

service@oalib.com

QQ:3279437679

WhatsApp +8615387084133