
leanTAP
 Referenced in 40 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...

KLONE
 Referenced in 41 articles
[sw28891]
 closely related to propositional modal logics and logics of programs (such as propositional dynamic logic ... from runofthemill modal and program logics. Consequently, the research on tableau algorithms ... logics led to new techniques and results, which are, however, also of interest for modal ... that play an important rôle in description logics (number restrictions, terminological axioms, and role constructors...

MiniML
 Referenced in 47 articles
[sw29625]
 type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying ... that bindingtime correctness is equivalent to modal correctness on this fragment. In addition, Mini...

SQEMA
 Referenced in 39 articles
[sw03056]
 Algorithmic correspondence and completeness in modal logic. IV. Semantic extensions of SQEMA ... firstorder equivalents and proving canonicity of modal formulae, and thus established a very general...

TABLEAUX
 Referenced in 18 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...

ModLeanTAP
 Referenced in 19 articles
[sw12368]
 Lean Tableaubased 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 tableaubased prover for firstorder logic leanTAP. ModLeanTAP Version 2.0 includes additional search...

CoLoSS
 Referenced in 14 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...

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

QMLTP
 Referenced in 10 articles
[sw09915]
 QMLTP problem library for firstorder modal logics. The Quantified Modal Logic Theorem Proving (QMLTP ... proving (ATP) systems for firstorder 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 multimodal logic are included as well...

MCMASSLK
 Referenced in 19 articles
[sw24778]
 labelling algorithm for epistemic and strategy logic modalities. We provide details of the checker which...

Spartacus
 Referenced in 15 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 12 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...

MleanCoP
 Referenced in 8 articles
[sw21522]
 connection prover for firstorder modal logic. MleanCoP is a fully automated theorem prover ... firstorder modal logic. The proof search is based on a prefixed connection calculus ... captures the Kripke semantics of different modal logics. MleanCoP is implemented in Prolog ... lines. It supports the standard modal logics D, T, S4, and S5 with constant, cumulative...

LoTREC
 Referenced in 27 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 12 articles
[sw14749]
 preorders; define propositions in a powerful modal logic and check whether a given process satisfies...

embed_modal
 Referenced in 4 articles
[sw28304]
 Theorem provers for every normal modal logic. We present a procedure for algorithmically embedding problems ... formulated in higherorder modal logic into classical higherorder logic. The procedure was implemented ... theorem provers into provers for various modal logics. The choice of the concrete modal logic ... accomplish the most widely applicable modal logic theorem prover available to date, i.e. no other...

evt
 Referenced in 8 articles
[sw09805]
 formulated as behavioural properties in a modal logic with recursion. We give a summary...

GoedelGod
 Referenced in 7 articles
[sw32223]
 existence is formalized in quantified modal logic KB (QML KB). QML KB is modeled...

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

InKreSAT
 Referenced in 6 articles
[sw23448]
 InKreSAT is a prover for the modal logics K, T, K4, and S4. InKreSAT reduces ... allows to integrate blocking mechanisms known from modal tableau provers. Blocking, in turn, further improves ... makes the approach applicable to the logics...