Michael Beeson's Research

Utility Link | Utility Link | Utility Link

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