Tarski Formalization Project Archives
Rays, and comparison of segments
$sameside(a,b,c)$ means that $a$ and $c$ are on the same side of point $b$, i.e. on the same ray emanating from $b$.
By definition that means $T(b,a,c)\lor T(b,c,a)$.
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 |
| Satz6.2a | Satz6.2a.prf | 11 | | | $a\neq b \land b\neq p \land c\neq p \land T(a,p,c) \land T(b,p,c) \rightarrow sameside(a,p,b)$ | | Satz6.2b | Satz6.2b.prf | 5 | | | $ a\neq b \land b\neq p \land c\neq p \land T(a,p,c) \land sameside(a,p,b)\rightarrow T(b,p,c) $ | | Satz6.3a | Satz6.3a.prf | 7 | | | $sameside(a,p,b)\rightarrow a\neq p \land b \neq p \land \exists c(c \neq p \land T(a,p,c) \land T(b,p,c)) $ | | Satz6.3b | Satz6.3b.prf | 1 | | | $a\neq p \land b \neq p \land \exists c(c \neq p \land T(a,p,c) \land T(b,p,c)) \rightarrow sameside(a,p,b)$ | | Satz6.4a | Satz6.4a.prf | 13 | | | $ sameside(a,p,b) \rightarrow Col(a,p,b) \land\neg T(a,p,b) $ | | Satz6.4b | Satz6.4b.prf | 11 | | | $Col(a,p,b) \land \neg T(a,p,b) \rightarrow sameside(a,p,b)$ | | Satz6.5 | Satz6.5.prf | 3 | | | (reflexivity) $a\neq p \rightarrow sameside(a,p,a) $ | | Satz6.6 | Satz6.6.prf | 5 | | | (symmetry) $sameside(a,p,b) \rightarrow sameside(b,p,a)$ | | Satz6.7 | Satz6.7.prf | 9 | | | (transitivity) $sameside(a,p,b) \land sameside(b,p,c) \rightarrow sameside(a,p,c)$ | | Satz6.11a | Satz6.11a.prf | 21 | diagram | | $r\neq a \land b\neq c \rightarrow \exists x(sameside(x,a,r) \land E(a,x,b,c)) $ | | Satz6.11b | Satz6.11b.prf | 17 | | | uniqueness of the $x$ in 6.11a | | Satz6.13a | Satz6.13a.prf | 11 | | | $sameside(a,p,b) \land pa \le pb \rightarrow T(p,a,b)$ | | Satz6.13b | Satz6.13b.prf | 1 | | | $sameside(a,p,b) \land T(p,a,b) \rightarrow pa \le pb $ | | Satz6.15a | Satz6.15a.prf | 10 | | | $ p\neq q \land p\neq r \land T(q,p,r) \land Col(p,q,a) \rightarrow sameside(a,p,q) or a=p or sameside(a,p,r)$ | | Satz6.15b | Satz6.15b.prf | 1 | | | $p\neq q \land p\neq r \land T(q,p,r) \land sameside(a,p,q) \rightarrow Col(p,q,a) $ | | Satz6.15c | Satz6.15c.prf | 9 | | | $p\neq q \land p\neq r \land T(q,p,r) \land sameside(a,p,r) \rightarrow Col(p,q,a) $ | | Satz6.15d | Satz6.15d.prf | 1 | | | $p\neq q \land p\neq r \land T(q,p,r) \land a=p \rightarrow Col(p,q,a) $ | | Satz6.16a | Satz6.16a.prf | 8 | | | $p\neq q \land p\neq r \land T(q,p,r) \land a=p \rightarrow Col(p,q,a) $ | | Satz6.16b | Satz6.16b.prf | 29 | subformula | 1881 | $p\neq q \land s\neq p \land Col(p,q,s) \land Col(p,q,x) \rightarrow Col(p,s,x)$ | | Satz6.17a | Satz6.17a.prf | 1 | | | $p\neq q \rightarrow Col(p,q,p)$ | | Satz6.17b | Satz6.17b.prf | 1 | | | $ p\neq q \land Col(p,q,x) \rightarrow Col(q,p,x) $ | | Satz6.18 | Satz6.18.prf | 19 | | | $ a\neq b \land p\neq q \land Col(p,q,a) \land Col(p,q,b) \land Col(p,q,x) \rightarrow Col(a,b,x)$.
This is a special case of Satz 6.21, used in proving Satz 6.21. | | Satz6.21 | Satz6.21.prf | 9 | | | If $Line(p,q)$ and $Line(a,b)$ have two different points in common then they coincide. | | Satz6.25 | Satz6.25.prf | 3 | | | There exists a point $x$ not on $Line(p,q)$, that is, such that not $Col(p,q,x)$. | | Satz6.28 | Satz6.28.prf | 21 | hints | | If $sameside(a,b,c)$ and $sameside(a1,b1,c1)$, and $ba$ and $bc$ are respectively
congruent to $b_1a_1$ and $b_1c_1$, then $ac$ is congruent to $a_1c_1$.
This is used in Satz 11.4, but is never proved in the book, and belongs in Chapter 6,
so we give it the name Satz 6.28. |
Back to top of archive
|
