On the mechanization of the proof of Hessenberg's theorem in coherent logic (Q2471743)

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.