A Vernacular for Coherent Logic

DOI10.1007/978-3-319-08434-3_28zbMath1304.68163arXiv1405.3391OpenAlexW2128184640MaRDI QIDQ5495937

Predrag Janičić, Sana Stojanović, Julien Narboux, Marc Bezem

Publication date: 7 August 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1405.3391

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Knowledge representation (68T30) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

Current Status of the I2GATP Common Format, From informal to formal proofs in Euclidean geometry, Automated generation of illustrated proofs in geometry and beyond, Towards an intelligent and dynamic geometry book, Theorem proving as constraint solving with coherent logic, Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry

Uses Software

• Coq
• Isabelle/Isar
• TPTP
• Isar
• Sledgehammer
• OMDoc
• ArgoCLP
• PRocH
• miz3

Cites Work

• Unnamed Item
• Obvious inferences
• Extending Sledgehammer with SMT solvers
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
• A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
• Automatic Proof and Disproof in Isabelle/HOL
• Skolem Machines and Geometric Logic
• Tarski's System of Geometry
• PRocH: Proof Reconstruction for HOL Light
• The challenge of computer mathematics
• Scalable LCF-Style Proof Translation
• Automating Coherent Logic
• Importing HOL Light into Coq
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS