Implementing tableau calculi using BDDs: BDDTab system description

DOI10.1007/978-3-319-08587-6_25MaRDI QIDQ3192204zbMATH OpenOpenAlexFDO

Authors Rajeev Goré, Kerry Olesen, Jimmy Thomson

Publication date 26 September 2014

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08587-6_25

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27) Mechanization of proofs and logical operations (03B35)

Recommendations

• BDD-based decision procedures for the modal logic K ★
• Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
• TABLEAUX: A general theorem prover for modal logics
• scientific article; zbMATH DE number 2090285
• Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K

Cited in

(10)

• Verified Decision Procedures for Modal Logics.
• CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
• scientific article; zbMATH DE number 1765664 (Why is no real title available?)
• \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal K
• Verified tableaux: from modal logics to modal fixpoint logics
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
• Optimizing a BDD-based modal solver.
• Non-classical logics in satisfiability modulo theories
• Resolution calculi for non-normal modal logics

Describes a project that uses

Uses Software

• BDDTab

This page was built for publication: Implementing tableau calculi using BDDs: BDDTab system description

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