A new theorem discovered by computer prover (Q583606)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A new theorem discovered by computer prover |
scientific article |
Statements
A new theorem discovered by computer prover (English)
0 references
1989
0 references
It is shown that some interesting theorems concerning Pappus lines and Leisenring lines can be easily proved by computer prover which is implemented on the basis of Wu's method for mechanical theorem proving in geometries. Using this prover a new theorem is discovered: The six intersection points of every Pappus line and its corresponding Leisenring line are collinear.
0 references
Pappus lines
0 references
Leisenring lines
0 references
mechanical theorem proving
0 references
