• 论文 • 上一篇    下一篇

构造型几何定理及其机器证明系统

王东明(1);胡森(2)   

  1. (1)中国科学院系统科学研究所;(2)中国科学院系统科学研究所
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:1987-04-25 发布日期:1987-04-25

王东明;胡森. 构造型几何定理及其机器证明系统[J]. 系统科学与数学, 1987, 7(2): 163-172.

WANG DONG-MING ;HU SEN. A MECHANICAL PROVING SYSTEM FOR CONSTRUCTIBLE THEOREMS IN ELEMENTARY GEOMETRY[J]. Journal of Systems Science and Mathematical Sciences, 1987, 7(2): 163-172.

A MECHANICAL PROVING SYSTEM FOR CONSTRUCTIBLE THEOREMS IN ELEMENTARY GEOMETRY

WANG DONG-MING (1);HU SEN(2)   

  1. (1)Institute of Systems Science,Academia Sinica;(2)Institute of Systems Science,Academia Sinica
  • Received:1900-01-01 Revised:1900-01-01 Online:1987-04-25 Published:1987-04-25
Hilbert 机械化定理表明,Pascal 几何中构造型交点定理可以机器证明。1982年,吴文俊教授给出了机械化定理的构造性证法。本文指出,通过添加若干新的构造类型,有更广泛的一类平面几何定理,其机器证明可以按照同样的构造性证法实现,我们称这类定理为构造型几何定理。作者适当调整吴文俊算法的步骤,在 HP1000小型计算机上建立了构造型几何定理的机器证明系统,效率大大提高,从而成功地证明了许多不平凡的几何定理,并且独立发现了相当深入的结果。
关键词:
In this paper,we point out that Hilbert's Mechanization Theorem may be extended to allconstructible theorems which can be mechanically proved in the same way by adjoining somenew constructive types.Using the Theorem-Prover built by the authors in rearranging thesteps of Wu's algorithm,many non-trivial theorems have been proved and some new resultshave also been discovered independently.
Key words:
()
[1] 阎春钢. 张量乘积图的同构因子分解[J]. 系统科学与数学, 1997, 17(4): 303-306.
[2] 徐士英. 关于弱拟凸集与广义凸集逼近的几点注记[J]. 系统科学与数学, 1997, 17(4): 372-375.
[3] 李学敏. 平面n次微分系统高次奇点的拓扑结构[J]. 系统科学与数学, 1997, 17(4): 311-315.
[4] 颜振标. 局部环上辛变换关于辛平延的分解[J]. 系统科学与数学, 2006, 26(2): 159-168.
[5] 向叔文. Banach压缩映象原理与空间完备性[J]. 系统科学与数学, 1997, 17(4): 307-310.
[6] 刘文. 对数似然比与整值随机变量序列的一类强律[J]. 系统科学与数学, 1997, 17(4): 316-323.
[7] 解学军;张正强. 多变量系统的基于矩阵$K_{P}=LDU$分解的鲁棒模型参考自适应控制[J]. 系统科学与数学, 2006, 26(2): 206-216.
[8] 王朝珠. 带有结构性不确定的线性时变系统的二次镇定及H~∞控制[J]. 系统科学与数学, 1997, 17(4): 330-337.
[9] 钟同德. Stein流形上的Lewy方程[J]. 系统科学与数学, 1997, 17(4): 289-297.
[10] 朱传喜;朱天. Z-P-S空间中的若干概率分析问题[J]. 系统科学与数学, 2006, 26(1): 1-004.
[11] 孙继涛. 区间周期系统的平稳振荡[J]. 系统科学与数学, 1997, 17(3): 208-212.
[12] 王培. 推点与二部竞赛图的强连通性[J]. 系统科学与数学, 2006, 26(1): 5-010.
[13] 周正新;俞元洪. 非线性微分系统的Poincare映射与周期解[J]. 系统科学与数学, 2006, 26(1): 59-068.
[14] 丁春梅. Bernstein型算子加Jacobi权逼近[J]. 系统科学与数学, 2006, 26(1): 11-020.
[15] 董亚丽;齐玉峰. 一类非线性系统的局部镇定[J]. 系统科学与数学, 2007, 27(2): 265-272.
阅读次数
全文


摘要