Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
From MaRDI portal
Publication:5505551
DOI10.1007/978-3-540-89439-1_12zbMath1182.68212OpenAlexW1579056021MaRDI QIDQ5505551
Sean McLaughlin, Frank Pfenning
Publication date: 27 January 2009
Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-89439-1_12
Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items (8)
Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations ⋮ Unnamed Item ⋮ Goal-oriented proof-search in natural deduction for intuitionistic propositional logic ⋮ Focused proof-search in the logic of bunched implications ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ Focused Inductive Theorem Proving ⋮ Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method ⋮ Focused and Synthetic Nested Sequents
Uses Software
Cites Work
This page was built for publication: Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
