Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic

DOI10.1007/978-3-540-89439-1_12MaRDI QIDQ5505551zbMATH OpenOpenAlexFDO

Authors 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

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35)

Recommendations

• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• Automated Deduction – CADE-20
• The inverse method application for non-classical logics
• Focusing and Polarization in Intuitionistic Logic
• A logical characterization of forward and backward chaining in the inverse method

Cites work

• OTTER

Cited in

(12)

• A forward unprovability calculus for intuitionistic propositional logic
• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• Focused proof-search in the logic of bunched implications
• Focused and Synthetic Nested Sequents
• Intuitionistic Decision Procedures Since Gentzen
• Disproving using the inverse method by iterative refinement of finite approximations
• fCube: an efficient prover for intuitionistic propositional logic
• Linking focusing and resolution with selection
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• Automated Deduction – CADE-20
• Focused Inductive Theorem Proving
• Skolemisation for intuitionistic linear logic

Describes a project that uses

Uses Software

• OTTER
• Imogen
• STRIP
• ILTP
• Twelf

This page was built for publication: Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic

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