First-order modal tableaux
From MaRDI portal
Recommendations
Cited in
(52)- On the intuitionistic force of classical search (extended abstract)
- On the modal logic K plus theories
- Reasoning with preorders and dynamic sorts using free variable tableaux
- Ground and free-variable tableaux for variants of quantified modal logics
- Decidability and complexity of simultaneous rigid E-unification with one variable and related results
- On the intuitionistic force of classical search
- scientific article; zbMATH DE number 3877148 (Why is no real title available?)
- Automated Reasoning with Analytic Tableaux and Related Methods
- Labelling ideality and subideality
- Implementing a relational theorem prover for modal logic K
- scientific article; zbMATH DE number 1543300 (Why is no real title available?)
- Resolution theorem proving in reified modal logics
- scientific article; zbMATH DE number 2099381 (Why is no real title available?)
- A simple tableau system for the logic of elsewhere
- Distributed modal theorem proving with KE
- scientific article; zbMATH DE number 1507180 (Why is no real title available?)
- Implementing and evaluating provers for first-order modal logics
- Proof-terms for classical and intuitionistic resolution
- Encoding First Order Proofs in SAT
- Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems
- scientific article; zbMATH DE number 922622 (Why is no real title available?)
- The liberalized -rule in free variable semantic tableaux
- scientific article; zbMATH DE number 1612550 (Why is no real title available?)
- Tableau calculus for local cubic modal logic and its implementation
- scientific article; zbMATH DE number 5295699 (Why is no real title available?)
- Free-variable tableaux for propositional modal logics
- Uniform and non uniform strategies for tableaux calculi for modal logics
- A tableau-like proof procedure for normal modal logics
- First-order tableaux in applications (extended abstract)
- Free variable tableaux for propositional modal logics
- The Tableau Workbench
- MGTP: a model generation theorem prover. Its advanced features and applications
- scientific article; zbMATH DE number 1950267 (Why is no real title available?)
- Hintikka multiplicities in matrix decision methods for some propositional modal logics
- LotrecScheme
- Accelerating tableaux proofs using compact representations
- scientific article; zbMATH DE number 1612541 (Why is no real title available?)
- Cut-free sequent and tableau systems for propositional Diodorean modal logics
- scientific article; zbMATH DE number 1761417 (Why is no real title available?)
- A logic for reasoning with inconsistency
- Certification of prefixed tableau proofs for modal logic
- scientific article; zbMATH DE number 440107 (Why is no real title available?)
- Strongly analytic tableaux for normal modal logics
- Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K
- \textsc{MetTeL}: a tableau prover with logic-independent inference engine
- The undecidability of simultaneous rigid E-unification
- Modal tableau systems with blocking and congruence closure
- MleanCoP: a connection prover for first-order modal logic
- Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
- Labelled proofs for quantified modal logic
- Theorem provers for every normal modal logic
- A First Order Extension of Stålmarck’s Method
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)
