First-order modal tableaux
From MaRDI portal
We describe simple semantic tableau based theorem provers for four standard modal logics, in both propositional and first-order versions. These theorem provers are easy to implement in Prolog, have a behavior that is straightforward to understand, and provide natural places for the incorporation of heuristics. Background theory is presented, and implementations of one propositional and one first-order version are given.
Recommendations
Cited in
(58)- TABLEAUX: A general theorem prover for modal logics
- A tableau-like proof procedure for normal modal logics
- Resolution theorem proving in reified modal logics
- Accelerating tableaux proofs using compact representations
- Cut-free sequent and tableau systems for propositional Diodorean modal logics
- The liberalized -rule in free variable semantic tableaux
- Decidability and complexity of simultaneous rigid E-unification with one variable and related results
- On the intuitionistic force of classical search
- Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
- scientific article; zbMATH DE number 1612541 (Why is no real title available?)
- scientific article; zbMATH DE number 1612550 (Why is no real title available?)
- LotrecScheme
- Implementing a relational theorem prover for modal logic K
- First-order tableaux in applications (extended abstract)
- \textsc{MetTeL}: a tableau prover with logic-independent inference engine
- scientific article; zbMATH DE number 440107 (Why is no real title available?)
- MleanCoP: a connection prover for first-order modal logic
- scientific article; zbMATH DE number 3877148 (Why is no real title available?)
- Modal tableau systems with blocking and congruence closure
- Implementing and evaluating provers for first-order modal logics
- scientific article; zbMATH DE number 5295699 (Why is no real title available?)
- Encoding First Order Proofs in SAT
- Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems
- Relations between propositional normal modal logics: an overview
- A description of the tableau method using abstract state machines
- lean TAP revisited
- scientific article; zbMATH DE number 1950267 (Why is no real title available?)
- scientific article; zbMATH DE number 1507180 (Why is no real title available?)
- scientific article; zbMATH DE number 1543300 (Why is no real title available?)
- scientific article; zbMATH DE number 1761417 (Why is no real title available?)
- MGTP: a model generation theorem prover. Its advanced features and applications
- Free variable tableaux for propositional modal logics
- Hintikka multiplicities in matrix decision methods for some propositional modal logics
- Labelling ideality and subideality
- Distributed modal theorem proving with KE
- A simple tableau system for the logic of elsewhere
- On the intuitionistic force of classical search (extended abstract)
- Theorem provers for every normal modal logic
- Proof-terms for classical and intuitionistic resolution
- Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K
- scientific article; zbMATH DE number 2099381 (Why is no real title available?)
- Uniform and non uniform strategies for tableaux calculi for modal logics
- scientific article; zbMATH DE number 881599 (Why is no real title available?)
- scientific article; zbMATH DE number 922622 (Why is no real title available?)
- Tableau calculus for local cubic modal logic and its implementation
- The Tableau Workbench
- Certification of prefixed tableau proofs for modal logic
- Tableau-based translation from first-order logic to modal logic
- Strongly analytic tableaux for normal modal logics
- Labelled proofs for quantified modal logic
- A First Order Extension of Stålmarck’s Method
- Automated Reasoning with Analytic Tableaux and Related Methods
- Free-variable tableaux for propositional modal logics
- Ground and free-variable tableaux for variants of quantified modal logics
- On the modal logic K plus theories
- Reasoning with preorders and dynamic sorts using free variable tableaux
- The undecidability of simultaneous rigid E-unification
- A logic for reasoning with inconsistency
This page was built for publication: First-order modal tableaux
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1104913)
