构造型几何定理及其机器证明系统
A MECHANICAL PROVING SYSTEM FOR CONSTRUCTIBLE THEOREMS IN ELEMENTARY GEOMETRY作者机构：中国科学院系统科学研究所 中国科学院系统科学研究所
出 版 物：《系统科学与数学》 (Journal of Systems Science and Mathematical Sciences)
年 卷 期：1987年第2期
页 面：163-172页
主 题：定理证明 人工智能 机器证明 几何定理 多项式方程 构造型 消去 非退化 方程组 联立方程 项数
摘 要：Hilbert 机械化定理表明,Pascal 几何中构造型交点定理可以机器证明。1982年,吴文俊教授给出了机械化定理的构造性证法。本文指出,通过添加若干新的构造类型,有更广泛的一类平面几何定理,其机器证明可以按照同样的构造性证法实现,我们称这类定理为构造型几何定理。作者适当调整吴文俊算法的步骤,在 HP1000小型计算机上建立了构造型几何定理的机器证明系统,效率大大提高,从而成功地证明了许多不平凡的几何定理,并且独立发现了相当深入的结果。
同方期刊数据库