Paper: On Mechanical Theorem Proving in Minkowskian Plane Geometry (at LICS 1986)

Authors: Shang-Ching Chou Hai-Ping Ko

Abstract

We report a successful experiment of mechanical theorem proving in Minkowskian plane geometry. We proved at least 40 theorems in Minkowskian geometry using the method of Wu Wen-Tsün for mechanical theorem proving in elementary geometry. We found that many famous theorems in Euclidean geometry, such as Simson's theorem, the Butterfly theorem, Euler's theorem, the 9-point circle theorem and Feuerbach's theorem are also valid in Minkowskian geometry. This surprising result led us to discover and establish a meta theorem which asserts that certain kinds of geometric statements can be confirmed to be true by the elementary part of Wu's method in Euclidean geometry iff they can be confirmed to be true by the elementary part of Wu's method in Minkowskian geometry.

BibTeX

  @InProceedings{ChouKo-OnMechanicalTheorem,
    author = 	 {Shang-Ching Chou and Hai-Ping Ko},
    title = 	 {On Mechanical Theorem Proving in Minkowskian Plane Geometry},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {187--192},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }