TABLEAUX: A general theorem prover for modal logics

DOI10.1007/BF01880326zbMath0743.03008MaRDI QIDQ1181709

Laurent Catach

Publication date: 27 June 1992

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

propositional modal logicsdynamic logictemporal logicPrologepistemic logictest examplesexperimental resultssemantic tableauxdecision proceduregeneral theorem proving systemmultimodal language

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Related Items

A tableau-like proof procedure for normal modal logics, Resolution theorem proving in reified modal logics, MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description), Uniform and non uniform strategies for tableaux calculi for modal logics, LINEAR TIME IN HYPERSEQUENT FRAMEWORK, A resolution-based proof method for temporal logics of knowledge and belief, Intuitionistic Decision Procedures Since Gentzen, Distributed modal theorem proving with KE, A simple tableau system for the logic of elsewhere, Proofs and countermodels in non-classical logics, Model Theoretic Syntax and Parsing, Strongly analytic tableaux for normal modal logics, An empirical analysis of modal theorem provers, TABLEAUX, A new method for testing decision procedures in modal logics, A uniform tableaux method for nonmonotonic modal logics, Local reductions for the modal cube, Proof analysis in modal logic

Uses Software

• KRIPKE

Cites Work

• The temporal logic of branching time
• Proof methods for modal and intuitionistic logics
• Handbook of philosophical logic. Volume II: Extensions of classical logic
• Interpreting logics of knowledge in propositional dynamic logic
• A decision procedure for combinations of propositional temporal logic and other specialized theories
• Modal resolution in clausal form
• Decidability for branching time
• Program analysis and optimization through kernel-control decomposition
• Propositional dynamic logic of regular programs
• Decision procedures and expressiveness in the temporal logic of branching time
• Expressiveness and completeness of an interval tense logic
• Temporal logic can be more expressive
• Synthesis of Communicating Processes from Temporal Logic Specifications
• The decision problem for branching time logic
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Deciding full branching time logic
• The complexity of propositional linear temporal logics
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item