Sketch-as-proof

MaRDI QIDQ4364520zbMATH OpenFDO

Authors Norbert Preining

Publication date 7 January 1998

zbMATH Keywords

cut-eliminationextension of Gentzen's LKprojective geometrysketches

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Cut-elimination and normal-form theorems (03F05) General theory of linear incidence geometry and projective geometries (51A05)

Recommendations

• Combinatorial analysis of proofs in projective and affine geometry
• Two cryptomorphic formalizations of projective incidence geometry
• Formalizing projective plane geometry in Coq
• Mechanical theorem proving in projective geometry
• Automated theorem proving in projective geometry with bracket algebra

Cited in

(3)

• scientific article; zbMATH DE number 1088533 (Why is no real title available?)
• Types for Proofs and Programs
• Axiomatizing the skew Boolean propositional calculus

This page was built for publication: Sketch-as-proof

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4364520)