A new method for testing decision procedures in modal logics

DOI10.1007/3-540-63104-6_26zbMath1430.68409OpenAlexW1569966280MaRDI QIDQ5234709

Roberto Sebastiani, Marco Roveri, 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

modal logicdecision proceduremodal depthsearch spacepropositional atom

Mathematics Subject Classification ID

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

Uses Software

• TABLEAUX

Cites Work

• Unnamed Item
• TABLEAUX: A general theorem prover for modal logics
• A guide to completeness and complexity for modal logics of knowledge and belief
• Exploiting the deep structure of constraint problems
• The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic
• Critical Behavior in the Satisfiability of Random Boolean Expressions
• Building decision procedures for modal logics from propositional decision procedures — The case study of modal K
• Uniform and non uniform strategies for tableaux calculi for modal logics

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