Tarski Formalization Project Archives
The posted input files are now all mechanically generated from a master list of theorems.
The times shown in the following table are not the times required to find the proof, but rather
the maximum time allocated to Otter to find the proof. The time is shown only when it had to be longer than
the default, which was often 20 seconds when hints were used and 120 seconds when hints were not used.
For more information about our methodology see the top page of this project.
| Input File |
Proof |
Length |
Strategy |
Seconds |
Commentary |
| Satz2.1 | Satz2.1.prf | 1 | | | (reflexivity) $E(a,b,a,b)$ | | Satz2.2 | Satz2.2.prf | 1 | | | (symmetry) $E(a,b,c,d) \rightarrow E(c,d,a,b)$ | | Satz2.3 | Satz2.3.prf | 2 | | | (transitivity) $E(a,b,c,d) \land E(c,d,e,f) \rightarrow E(a,b,e,f)$ | | Satz2.4 | Satz2.4.prf | 1 | | | $E(a,b,c,d) \rightarrow E(b,a,c,d)$ | | Satz2.5 | Satz2.5.prf | 1 | | | $E(a,b,c,d) \rightarrow E(a,b,d,c)$ | | Satz2.8 | Satz2.8.prf | 3 | | | $E(a,a,b,b)$ (all null segments are congruent) | | Satz2.11 | Satz2.11.prf | 14 | | | $T(a,b,c,) \land T(a1,b1,c1) \land E(a,b,a1,b1) \land E(b,c,b1,c1) \rightarrow E(a,c,a1,c1)$ | | Satz2.12 | Satz2.12.prf | 5 | | | (uniqueness of segment extension)
$ q!=a \land T(q,a,x) \land E(a,x,b,c) \land T(q,a,y) \land E(a,y,b,c) \rightarrow x=y$ | | Satz2.13 | Satz2.13.prf | 1 | | | $ E(x,y,u,u) \rightarrow x=y.$ Anything congruent to a null segment is a null segment.This theorem does not occur in the book, and we don't actually need it, but it seems pretty basic. | | Satz2.14 | Satz2.14.prf | 2 | | | $E(x,y,u,v) \rightarrow E(y,x,v,u)$.
This theorem does not occur in the book, but we need it in Satz 10.12a and Satz 11.15b. | | Satz2.15 | Satz2.15.prf | 13 | hints | | $T(a,b,c) \land T(A,B,C) \land E(a,b,B,C) \land E(b,c,A,B) \rightarrow E(a,c,A,C)$.
This theorem, very similar to 2.11, does not occur in the book, but we need it in Satz 11.15b.
It can be proved very easily using Satz 3.1, but here we prove it without Satz 3.1, which is not quite trivial. |
Back to top of archive
|
