Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method

DOI10.1007/978-3-642-02959-2_19zbMath1250.03019OpenAlexW1604435911MaRDI QIDQ5191105

Sean McLaughlin, Frank Pfenning

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_19

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

From axioms to synthetic inference rules via focusing, Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations, Structural Focalization, Theorem prover for intuitionistic logic based on the inverse method

Uses Software

• ILTP
• TPTP
• Twelf
• ileanCoP
• Imogen

Cites Work

• The ILTP problem library for intuitionistic logic
• A logical characterization of forward and backward chaining in the inverse method
• The TPTP problem library. CNF release v1. 2. 1
• Focussing and proof construction
• Focusing and higher-order abstract syntax
• Focusing and Polarization in Intuitionistic Logic
• Logic Programming with Focusing Proofs in Linear Logic
• Computer Science Logic
• Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item