Eighth Annual IEEE Symposium on

Logic in Computer Science (LICS 1993)

Paper: Automated production of traditional proofs for constructive geometry theorems (at LICS 1993)

Authors: Shang-Ching Chou Xiao-Shan Gao Jing-Zhong Zhang


The authors present a method that can produce traditional proofs for a class of geometry statements whose hypotheses can be described constructively and whose conclusions can be represented by polynomial equations of three kinds of geometry quantities: ratios of lengths, areas of triangles, and Pythagoras differences of triangles. This class covers a large portion of the geometry theorems about straight lines and circles. The method involves the elimination of the constructed points from the conclusion using a few basic geometry propositions. The authors' program, Euclid, implements this method and can produce traditional proofs of many hard geometry theorems. Currently, it has produced proofs of 400 nontrivial theorems entirely automatically, and the proofs produced are generally short and readable. This method seems to be the first one to produce traditional proofs for hard geometry theorems efficiently


    author = 	 {Shang-Ching Chou and Xiao-Shan Gao and Jing-Zhong Zhang},
    title = 	 {Automated production of traditional proofs for constructive geometry theorems },
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {48--56},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}