A new method for testing decision procedures in modal logics

DOI10.1007/3-540-63104-6_26MaRDI QIDQ5234709zbMATH OpenOpenAlexFDO

Authors Marco Roveri, Roberto Sebastiani, Fausto Giunchiglia

Publication date 1 October 2019

Published in Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-63104-6_26

zbMATH Keywords

decision proceduremodal depthmodal logicpropositional atomsearch space

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A guide to completeness and complexity for modal logics of knowledge and belief
• Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K
• Critical Behavior in the Satisfiability of Random Boolean Expressions
• Exploiting the deep structure of constraint problems
• scientific article; zbMATH DE number 1995157 (Why is no real title available?)
• TABLEAUX: A general theorem prover for modal logics
• The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic
• Uniform and non uniform strategies for tableaux calculi for modal logics

Describes a project that uses

Uses Software

• TABLEAUX

This page was built for publication: A new method for testing decision procedures in modal logics

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