SAT-based proof search in intermediate propositional logics

DOI10.1007/978-3-031-10769-6_5MaRDI QIDQ2104497zbMATH OpenOpenAlexFDO

Authors Camillo Fiorentini, Mauro Ferrari

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

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)

Recommendations

• Efficient SAT-based proof search in intuitionistic propositional logic
• Proof-search in intuitionistic logic based on constraint satisfaction
• A proof-search procedure for intuitionistic propositional logic
• scientific article; zbMATH DE number 1753197
• scientific article; zbMATH DE number 1390270
• Proof-search in hybrid logic
• A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic
• scientific article; zbMATH DE number 1348467
• scientific article; zbMATH DE number 1696770
• Induction in saturation-based proof search

Cites work

• A history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description
• A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic
• Automated synthesis of tableau calculi
• BOUNDED-ANALYTIC SEQUENT CALCULI AND EMBEDDINGS FOR HYPERSEQUENT LOGICS
• CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
• Contraction-free sequent calculi for intuitionistic logic
• Efficient SAT-based proof search in intuitionistic propositional logic
• fCube: an efficient prover for intuitionistic propositional logic
• Generalized tableau systems for intermediate propositional logics
• Gödel-Dummett counter-models through matrix computation
• scientific article; zbMATH DE number 1003731 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• SAT modulo intuitionistic implications
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Strongly equivalent logic programs
• Terminating calculi for propositional Dummett logic with subformula property

Cited in

(6)

• Efficient SAT-based proof search in intuitionistic propositional logic
• Satallax: An Automatic Higher-Order Prover
• SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions
• scientific article; zbMATH DE number 4094866 (Why is no real title available?)
• General clauses for SAT-based proof search in intuitionistic propositional logic
• Labelled KE for intuitionistic propositional logic

Describes a project that uses

Uses Software

• fCube
• IntHistGC
• intuit

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

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