Implementing a relational theorem prover for modal logic K
From MaRDI portal
Recommendations
- Relational dual tableau decision procedure for modal logic K
- \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
- scientific article; zbMATH DE number 1765692
- An efficient relational deductive system for propositional non-classical logics
- First-order modal tableaux
Cites work
- A benchmark method for the propositional modal logics K, KT, S4
- A new deduction system for deciding validity in modal logic K
- A proof system for contact relation algebras
- An efficient relational deductive system for propositional non-classical logics
- An implementation of a dual tableaux system for order-of-magnitude qualitative reasoning
- An on-the-fly tableau-based decision procedure for PDL-satisfiability
- Dual tableau for a multimodal logic for order of magnitude qualitative reasoning with bidirectional negligibility
- lean\(T^ AP\): Lean tableau-based deduction
- On Automating the Calculus of Relations
- Proof analysis in modal logic
- Rasiowa-Sikorski deduction systems in computer science applications.
- Relational approach for a logic for order of magnitude qualitative reasoning with negligibility, non-closeness and distance
- Relational dual tableaux for interval temporal logics
- Relational proof system for relevant logics
- Single step tableaux for modal logics. Computational properties, complexity and methodology
- The Tableau Workbench
Cited in
(9)- \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
- On the existence and unicity of stable models in normal residuated logic programs
- Minimal Proof Search for Modal Logic K Model Checking
- MleanCoP: a connection prover for first-order modal logic
- Relational dual tableau decision procedures and their applications to modal and intuitionistic logics
- scientific article; zbMATH DE number 881599 (Why is no real title available?)
- Relational dual tableau decision procedure for modal logic K
- Tableau calculus for local cubic modal logic and its implementation
- Dual tableau-based decision procedures for fragments of the logic of binary relations
This page was built for publication: Implementing a relational theorem prover for modal logic K
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3008387)
