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 |
| Satz4.2 | Satz4.2.prf | 44 | hints | | $ T(a,b,c) \land T(a_1,b_1,c_1) \land E(a,c,a_1,c_1) \land E(b,c,b_1,c_1).
\land E(a,d,a_1,d1) \land E(c,d,c_1,d1) \rightarrow E(b,d,b_1,d1)$
This is the ``inner five-segment theorem'', similar to the 5-segment axiom but
with the segments to be proved equal on the inside, rather than the outside. | | Satz4.3 | Satz4.3.prf | 4 | | 300 | $T(a,b,c) \land T(a_1,b_1,c_1) \land E(a,c,a_1,c_1) \land E(b,c,b_1,c_1) \rightarrow E(a,b,a_1,b_1) $ | | Satz4.5 | Satz4.5.prf | 24 | subformula | 60 | $T(a,b,c) \land ac = a_1c_1 \rightarrow \exists z(T(a_1,z,c_1) \land (a,b,c) \cong (a_1,z,c_1) $
We give an explicit term $insert(a,b,a_1,c_1)$ that produces $z$, so a new Skolem function is not needed. | | Satz4.6 | Satz4.6.prf | 11 | | | $ T(a,b,c) \land E(a,c,a_1,c_1) \rightarrow \exists b_1(T(a_1,b_1,c_1) \land E3(a,b,c,a_1,b_1,c_1)) $.
We also show that $b_1$ depends only on $a,b,a_1,c_1$ (not on $c$) by an explicit term. | | Satz4.11a | Satz4.11a.prf | 3 | | | $Col(a,b,c) \rightarrow Col(b,c,a) $ | | Satz4.11b | Satz4.11b.prf | 2 | | | similarly for all permutations of $(a,b,c)$ | | Satz4.11c | Satz4.11c.prf | 7 | | | $ $ | | Satz4.11d | Satz4.11d.prf | 2 | | | $ $ | | Satz4.11e | Satz4.11e.prf | 2 | | | $ $ | | Satz4.12 | Satz4.12.prf | 1 | | | $Col(a,a,b) $ | | Satz4.12b | Satz4.12b.prf | 1 | | | $ Col(a,b,a) $ | | Satz4.13 | Satz4.13.prf | 16 | | | $ Col(a,b,c) \land E3(a,b,c,a_1,b_1,c_1) \rightarrow Col(a_1,b_1,c_1) $ | | Satz4.14 | Satz4.14.prf | 27 | diagram | | $ Col(a,b,c) \land E(a,b,a_1,b_1) \rightarrow \exists c_1(E3(a,b,c,a_1,b_1,c_1)) $ | | Satz4.16 | Satz4.16.prf | 25 | hints | 300 | $Col(a,b,c) \land E3(a,b,c,a_1,b_1,c_1) \land E(a,d,a_1,d1)
\land E(b,d,b_1,d1) \land a\neq b \rightarrow E(c,d,c_1,d1) $ | | Satz4.17 | Satz4.17.prf | 2 | | | $ a\neq b \land Col(a,b,c) \land E(a,p,a,q) \land E(b,p,b,q) \rightarrow E(c,p,c,q) $ | | Satz4.18 | Satz4.18.prf | 5 | | | $ a\neq b \land Col(a,b,c) \land E(a,c,a,c_1) \land E(b,c,b,c_1) \rightarrow c = c_1 $ | | Satz4.19 | Satz4.19.prf | 12 | | | $ T(a,c,b) \land E(a,c,a,c_1) \land E(b,c,b,c_1) \rightarrow c = c_1 $ |
Back to top of archive
|
