A new theorem discovered by computer prover (Q583606)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: A new theorem discovered by computer prover |
scientific article; zbMATH DE number 4133012
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A new theorem discovered by computer prover |
scientific article; zbMATH DE number 4133012 |
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
0 references
0.83434194
0 references
0 references
