Strongly analytic tableaux for normal modal logics

DOI10.1007/3-540-58156-1_52zbMath1433.03026OpenAlexW1567530468MaRDI QIDQ5210808

Fabio Massacci

Publication date: 21 January 2020

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

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_52

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)

Related Items

First-order intensional logic, Labeled sequent calculi for modal logics and implicit contractions, Prefixed tableaus and nested sequents, Free variable tableaux for propositional modal logics, Hintikka multiplicities in matrix decision methods for some propositional modal logics, Tableaux methods for access control in distributed systems, Unnamed Item, Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse, Through an Inference Rule, Darkly, A simple tableau system for the logic of elsewhere, Building decision procedures for modal logics from propositional decision procedures — The case study of modal K, Tableaux and algorithms for Propositional Dynamic Logic with Converse, Hybrid Tableaux for the Difference Modality, A uniform tableaux method for nonmonotonic modal logics, Labelled tableau systems for some subintuitionistic logics, EXPtime tableaux for ALC, Combining deduction and model checking into tableaux and algorithms for converse-PDL., Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).

Uses Software

• TABLEAUX

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Theory matrices (for modal logics) using alphabetical monotonicity
• Proof methods for modal and intuitionistic logics
• On the relation between default and autoepistemic logic
• First-order modal tableaux
• TABLEAUX: A general theorem prover for modal logics
• Modelling knowledge and action in distributed systems
• Tableau methods of proof for modal logics
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Modal nonmonotonic logics