Tarski Formalization Project Archives
Extensionality and Perpendicularity
Szmielew treats lines as sets, so she omits some simple lemmas that are required in a formal treatment. These can be proved
quite easily as soon as perpendicularity is defined (which is in Chapter 8).
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 |
| ExtCol2 | ExtCol2.prf | 2 | | | If $c$ and $d$ are distinct points on $Line(a,b)$, then every point on $Line(c,d)$ is also on $Line(a,b)$. |
| ext1 | ext1.prf | 2 | | | If $Col(a,b,c)$ and $Col(a,b,d)$ and $ a \neq b$, then $Col(a,c,d)$. |
| ExtPerp | ExtPerp.prf | 36 | hints | | If $ab$ and $cd$ determine the same line and $perpAt(a,b,x,p,q)$ then $perpAt(c,d,x,p,q)$.
Used in 8.24 as well as subsequent chapters. |
| ExtPerp2 | ExtPerp2.prf | 7 | diagram | | If $p$ and $q$ lie on $Line(a,b)$ and $p \neq q$, then $pq \perp cd$ implies $ab \perp cd$. |
| ExtPerp3 | ExtPerp3.prf | 3 | | | If $a,b,c,d$ are distinct and $ba \perp ac$ and $Col(a,c,d)$ then $ba \perp ad$. |
| ExtPerp4 | ExtPerp4.prf | 3 | | | $ab \perp pq$ implies $ab \perp qp$. |
| ExtPerp5 | ExtPerp5.prf | 8 | | | If $p$ and $q$ lie on $Line(a,b)$ and $p \neq q$, then $ab \perp cd$ implies $pq \perp cd$. |
| ExtPerp6 | ExtPerp6.prf | 3 | | | If $p$ and $q$ lie on $Line(a,b)$ and $p \neq q$, then $cd \perp pq $ implies $cd \perp ab$. |
Back to top of archive
