Automated development of Tarski's geometry (Q1825046)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Automated development of Tarski's geometry |
scientific article |
Statements
Automated development of Tarski's geometry (English)
0 references
1989
0 references
The author uses McCune's automated reasoning system to prove theorems in Euclidean plane geometry within the framework of Tarski's axiomatization (this is a first-order axiomatization which was shown by Tarski to be complete and decidable). McCune's automated reasoning system OTTER is a resolution based theorem prover (hyperresolution was used in most cases) but it is not interactive. The author carefully comments about his choice of weight for retained clauses. He proved various ``challenge problems'' on a VAX 8800 and gives performance statistics for the challenge problems. In addition, he comments briefly upon the performance of a CRAY X-MP/14 and poses further challenge problems.
0 references
Tarski's geometry
0 references
mechanical theorem proving
0 references
automated reasoning
0 references
resolution
0 references