Efficient SAT-based proof search in intuitionistic propositional logic

DOI10.1007/978-3-030-79876-5_13OpenAlexW3178727120MaRDI QIDQ2055856

Camillo Fiorentini

Publication date: 1 December 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_13

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

SAT-based proof search in intermediate propositional logics

Cites Work

• Unnamed Item
• Unnamed Item
• The ILTP problem library for intuitionistic logic
• A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic
• Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
• Simplification Rules for Intuitionistic Propositional Tableaux
• A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description
• Solving SAT and SAT Modulo Theories
• SAT Modulo Intuitionistic Implications
• Contraction-free sequent calculi for intuitionistic logic
• fCube: An Efficient Prover for Intuitionistic Propositional Logic
• Duality between Unprovability and Provability in Forward Refutation-search for Intuitionistic Propositional Logic
• Theory and Applications of Satisfiability Testing

This page was built for publication: Efficient SAT-based proof search in intuitionistic propositional logic