On the mechanization of the proof of Hessenberg's theorem in coherent logic (Q2471743)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | On the mechanization of the proof of Hessenberg's theorem in coherent logic |
scientific article |
Statements
On the mechanization of the proof of Hessenberg's theorem in coherent logic (English)
0 references
18 February 2008
0 references
General-purpose automated theorem provers are not yet able to prove difficult theorems. The formal verification of difficult theorems requires human ingenuity. The authors propose to combine interactive proof construction with proof automation for a fragment of first-order logic called coherent logic (CL). CL allows to make Skolemization unnecessary and has a natural proof system based on forward reasoning. This approach was tested by formally proving Hessenberg's theorem in elementary projective plane geometry.
0 references
coherent logic
0 references
automated theorem proving
0 references
proof objects
0 references
Hessenberg's theorem
0 references
projective plane geometry
0 references
