谁知道几何机械证明程序
发布网友
发布时间：2024-05-06 12:08
共2个回答
热心网友
时间：2024-06-24 09:55
1. SC Chou, XS Gao and JZ Zhang, Machine Proofs in Geometry, Automated Production of Readable Proofs for Geometry Theorems, World Scientific, 1994.此书详细的说明面积方法、几何定理之机械化证明、立体几何之机械证明、向量方法及使用软体The Geometry Expert所证明的四百题几何命题之全部内容。 SC Chou, XS Gao and JZ Zhang, Machine Proofs in Geometry, Automated Production of Readable Proofs for Geometry Theorems, World Scientific, 1994.此书详细的说明面积方法、几何定理之机械化证明、立体几何之机械证明、向量方法及使用软体The Geometry Expert所证明的四百题几何命题之全部内容。 Robert S. Boyer称本书之出版为”the single most important event in automated reasoning since Slagle and Moses first implemented programs for symbolic integration.” Robert S. Boyer称本书之出版为”the single most important event in automated reasoning since Slagle and Moses first implemented programs for symbolic integration.”
2. SC Chou and XS Gao, Mechanical Formula Derivation in Elementary Geometry, Proc. ISSAC-90, ACM, New York, 1990, pp. 265-270.基於Groebner基底法与Ritt-Wu特徵法，作者提出三种求几何公式的方法。 SC Chou and XS Gao, Mechanical Formula Derivation in Elementary Geometry, Proc. ISSAC-90, ACM, New York, 1990, pp. 265-270.基于Groebner基底法与Ritt-Wu特征法，作者提出三种求几何公式的方法。
3. SC Chou, XS Gao and JZ Zhang, Automated Production of Traditional Proofs for Theorems in Euclidean Geometry, Proc. of Eighth IEEE Symposium on Logic in Computer Science, p.48-56, IEEE Computer Society Press, 1993.应用面积法探讨与垂直、圆相关之定理。 SC Chou, XS Gao and JZ Zhang, Automated Production of Traditional Proofs for Theorems in Euclidean Geometry, Proc. of Eighth IEEE Symposium on Logic in Computer Science, p.48-56, IEEE Computer Society Press, 1993.应用面积法探讨与垂直、圆相关之定理。 该方法实现於计算机上(Euclid)，可证明420条定理。 该方法实现于计算机上(Euclid)，可证明420条定理。
4. SC Chou, XS Gao and JZ Zhang, Automated Generation of Readable Proofs with Geometric Invariants, I. Mutiple and Shortest Proof Generation, Preprint.本文探讨高阶层几何辅助定理可用来解决简短且可读之几何证明，特别是多重的最短证明。 SC Chou, XS Gao and JZ Zhang, Automated Generation of Readable Proofs with Geometric Invariants, I. Mutiple and Shortest Proof Generation, Preprint.本文探讨高阶层几何辅助定理可用来解决简短且可读之几何证明，特别是多重的最短证明。 初步之程式产生『证明暴涨』之现象。 初步之程式产生『证明暴涨』之现象。 说明挑选最短证明之策略。 说明挑选最短证明之策略。 本文探讨Ceva-Menelaus构形。 本文探讨Ceva-Menelaus构形。
5. SC Chou, XS Gao and JZ Zhang, Automated Generation of Readable Proofs with Geometric Invariants, II. Theorem Proving with Full-Angles, Preprint.探讨全角法。 SC Chou, XS Gao and JZ Zhang, Automated Generation of Readable Proofs with Geometric Invariants, II. Theorem Proving with Full-Angles, Preprint.探讨全角法。
6. SC Chou, XS Gao and JZ Zhang, The Area Method and Affine Geometries over Any Fields, Preprint.作者说明面积方法除了欧氏平面几何外，也适用於其他域 SC Chou, XS Gao and JZ Zhang, The Area Method and Affine Geometries over Any Fields, Preprint.作者说明面积方法除了欧氏平面几何外，也适用于其他域
(包括有限域)之仿射几何。 (包括有限域)之仿射几何。 面积方法可应用於证明7 3 ,8 3 ,9 3 等构形之存在。 面积方法可应用于证明7 3 ,8 3 ,9 3 等构形之存在。
7. SC Chou, XS Gao and JZ Zhang, Automated Geometry Theorem Proving and Geometry Education, Proc. of the First Asian Technology Conference in Mathematics, Singapore, 1995, pp. 319-328.这是张景中在ATCM中所作的报告。 SC Chou, XS Gao and JZ Zhang, Automated Geometry Theorem Proving and Geometry Education, Proc. of the First Asian Technology Conference in Mathematics, Singapore, 1995, pp. 319-328.这是张景中在ATCM中所作的报告。
8. SC Chou, Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, 1988.开始的九十四页详细介绍吴文俊的机械证明法，其后之二百五十三页收集了五百一十二个计算机证明的几何命题。 SC Chou, Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, 1988.开始的九十四页详细介绍吴文俊的机械证明法，其后之二百五十三页收集了五百一十二个计算机证明的几何命题。
9. WT Wu, Basic Principles of Mechanical Theorem Proving in Geometries, Volume I: Part of Elementary Geometries, Science Press, 1984.本书共分六章，前两章是有关於几何机械化的知识(Desargues几何与Desargue数系，垂直几何、度量几何与常用几何)，后四章致力於几何机械化问题(Hilbert机械化定理、无序的几何机械化定理、有序的几何机械化定理、各种的几何机械化定理) WT Wu, Basic Principles of Mechanical Theorem Proving in Geometries, Volume I: Part of Elementary Geometries, Science Press, 1984.本书共分六章，前两章是有关于几何机械化的知识(Desargues几何与Desargue数系，垂直几何、度量几何与常用几何)，后四章致力于几何机械化问题(Hilbert机械化定理、无序的几何机械化定理、有序的几何机械化定理、各种的几何机械化定理)
10. WT Wu, On the Decision Problem and the Mechanization of Theorem-Proving in Elementary Geometry, Automated Theorem Proving: After 25 Years, Contemporary Mathematics, vol. 29, 1984, pp213-234.此文为1978年Scientia Sinica 21 (2)之再版。 WT Wu, On the Decision Problem and the Mechanization of Theorem-Proving in Elementary Geometry, Automated Theorem Proving: After 25 Years, Contemporary Mathematics, vol. 29, 1984, pp213-234.此文为1978年Scientia Sinica 21 (2)之再版。 A. Tarski於1951发表之”A decision method for elementary algebra and geometry”裏提出可决定的程序来证明定理。 A. Tarski于1951发表之”A decision method for elementary algebra and geometry”里提出可决定的程序来证明定理。 然而该程序不足够应对几何裏稍为难一点的定理。 然而该程序不足够应对几何里稍为难一点的定理。 在这篇文章裏吴文俊提出一套新的原理，与Tarski及其追随者Seidenberg、A. Robinson、PJ Cohen所依循的路线不一样。 在这篇文章里吴文俊提出一套新的原理，与Tarski及其追随者Seidenberg、A. Robinson、PJ Cohen所依循的路线不一样。 该原理可用来证明颇难之几何定理。 该原理可用来证明颇难之几何定理。 (基於该原理周咸青用PASCAL写成了证明器，在1985年已能证512条定理。) (基于该原理周咸青用PASCAL写成了证明器，在1985年已能证512条定理。)
热心网友
时间：2024-06-24 09:57
