• leanTAP

  • Referenced in 29 articles [sw09985]
  • generalizes the sequent calculus to the modal logic K and sketches a proof ... theorem prover for the modal logic K which is as elegant as leanTAP. Following that ... results can be obtained for the modal logics T, K4 and S4. The paper ... extended to the case of quantified modal logics as long as the Barcan formula...
  • ModLeanTAP

  • Referenced in 17 articles [sw12368]
  • Lean Tableau-based Deduction for Propositional Modal Logics. ModLeanTAP is a lean Prolog implementation ... modular labelled tableau calculus for propositional modal logics (where the labels contain free and universal ... with other considerably more complex implementations for modal deduction. ModLeanTAP’s development was inspired ... lean tableau-based prover for first-order logic leanTAP. ModLeanTAP Version 2.0 includes additional search...
  • SQEMA

  • Referenced in 23 articles [sw03056]
  • Algorithmic correspondence and completeness in modal logic. IV. Semantic extensions of SQEMA ... first-order equivalents and proving canonicity of modal formulae, and thus established a very general...
  • CoLoSS

  • Referenced in 9 articles [sw07016]
  • Solver CoLoSS, the Coalgebraic Logic Satisfiability Solver, decides satisfiability of modal formulas in a generic ... space algorithm to decide satisfiability for modal logics that are amenable to coalgebric semantics. This ... Pauly’s coalition logic, graded modal logic, and probabilistic modal logic. Logics are easily integrated ... that include the fusion of two modal logics as a special case. One thus automatically...
  • TABLEAUX

  • Referenced in 7 articles [sw11674]
  • TABLEAUX: A general theorem prover for modal logics. We present a general theorem proving system ... propositional modal logics, called TABLEAUX. The main feature of the system is its generality, since ... wide class of modal logics, including usual temporal, epistemic or dynamic logics. We survey ... such semantical proof methods for modal logics, since we believe that the model construction they...
  • MSPASS

  • Referenced in 11 articles [sw17667]
  • which can be used as a modal logic theorem prover, a theorem prover for description...
  • Spartacus

  • Referenced in 9 articles [sw12426]
  • tableau prover for hybrid multimodal logic with global modalities and reflexive and transitive relations. Spartacus ... lazy branching for the basic modal logic K and observe high effectiveness of both techniques...
  • HTab

  • Referenced in 8 articles [sw12427]
  • that is closely related to both modal logic and description logic. A variety of proof ... mechanisms for hybrid logic exist, but the only widely available implemented proof system, HyLoRes ... already widely used for both modal and description logics. Tableaux algorithms have also been developed...
  • LoTREC

  • Referenced in 17 articles [sw07684]
  • LoTREC: Logical tableaux research engineering companion In this paper we describe a generic tableaux system ... testing satisfiability of formulas in modal and description logics. This system is called LoTREC2.0...
  • Concurrency Workbench

  • Referenced in 8 articles [sw14749]
  • preorders; define propositions in a powerful modal logic and check whether a given process satisfies...
  • evt

  • Referenced in 5 articles [sw09805]
  • formulated as behavioural properties in a modal logic with recursion. We give a summary...
  • MLAT

  • Referenced in 3 articles [sw00582]
  • present an abstraction framework based on modal logic and predicate abstraction technique. In the framework ... employ modal logic 2CTLN in order to express predicates for abstraction and specifications of programs...
  • Mechanized Semantic Library

  • Referenced in 4 articles [sw13123]
  • useful for developing semantic models of program logics and type systems: separation algebras, permission share ... clean axiomatization of step indexing), and modal logics. The library has a special emphasis...
  • MoMo

  • Referenced in 4 articles [sw10020]
  • MoMo: A modal logic for reasoning about mobility. A temporal logic is proposed...
  • Sibyl

  • Referenced in 5 articles [sw11995]
  • automated theorem prover for multi-modal hibrid logic with binders, the converse and global modalities...
  • GQML

  • Referenced in 2 articles [sw11996]
  • general theorem prover for quantified modal logics. The main contribution of this work is twofold ... main domain variants of quantified modal logic and dealing with languages where rigid...
  • MGTP

  • Referenced in 3 articles [sw09701]
  • based theorem prover MGTP for first-order logic. This paper describes the major results ... negation as failure, abductive reasoning and modal logic systems, on MGTP. These techniques share...
  • HyLoRes

  • Referenced in 3 articles [sw17660]
  • prover for hybrid logics. These are modal-like logics with facilities to refer to objects ... modal (or hybrid) input, with no translation into background logics. HyLoRes fuses state...
  • QMLTP

  • Referenced in 1 article [sw09915]
  • QMLTP problem library for first-order modal logics. The Quantified Modal Logic Theorem Proving (QMLTP ... proving (ATP) systems for first-order modal logics. The main purpose of the library ... version 1.1 of the library the modal logics K, D, T, S4 and S5 with ... small number of problems for multi-modal logic are included as well...
  • ModalCasl

  • Referenced in 1 article [sw11951]
  • ModalCasl: Specification with Multi-Modal Logics. ModalCASL extends CASL by modal operators. Syntax for ordinary ... modalities, multi-modal logics as well as term-modal logic (also covering dynamic logic ... provided. Specific modal logics can be obtained via restrictions to sublanguages...