SAT-based proof search in intermediate propositional logics

DOI10.1007/978-3-031-10769-6_5OpenAlexW4289103993MaRDI QIDQ2104497

Camillo Fiorentini, Mauro Ferrari

Publication date: 7 December 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_5

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• fCube
• IntHistGC
• intuit

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Efficient SAT-based proof search in intuitionistic propositional logic
• CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
• A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic
• Terminating calculi for propositional Dummett logic with subformula property
• 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
• Generalized tableau systems for intermediate propositional logics
• fCube: An Efficient Prover for Intuitionistic Propositional Logic
• BOUNDED-ANALYTIC SEQUENT CALCULI AND EMBEDDINGS FOR HYPERSEQUENT LOGICS
• Strongly equivalent logic programs
• Automated Synthesis of Tableau Calculi

This page was built for publication: SAT-based proof search in intermediate propositional logics