A benchmark method for the propositional modal logics K, KT, S4
From MaRDI portal
Publication:1977575
DOI10.1023/A:1006249507577zbMath0955.03013OpenAlexW1593443951MaRDI QIDQ1977575
Peter Balsiger, Alain Heuerding, Stefan Schwendimann
Publication date: 17 January 2001
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1006249507577
Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)
Related Items
Proof complexity of modal resolution, An efficient approach to nominal equalities in hybrid logic tableaux, SYMMETRIES IN MODAL LOGICS, Mechanising Gödel-Löb provability logic in HOL light, Symmetric blocking, Unnamed Item, An Experimental Evaluation of Global Caching for $\mathcal {ALC}$ (System Description), Verified Decision Procedures for Modal Logics., Implementing a relational theorem prover for modal logic, Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic, A prover dealing with nominals, binders, transitivity and relation hierarchies, \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments, : A Resolution-Based Prover for Multimodal K, Efficient local reductions to basic modal logic, On coarser interval temporal logics, Local is best: efficient reductions to modal logic \textsf{K}, Local reductions for the modal cube, Efficient SAT-based minimal model generation methods for modal logic S5
Uses Software
