
KLONE
 Referenced in 41 articles
[sw28891]
 related to propositional modal logics and logics of programs (such as propositional dynamic logic ... applications, most description logics differ significantly from runofthemill modal and program logics...

ModLeanTAP
 Referenced in 19 articles
[sw12368]
 ModLeanTAP: 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...

TABLEAUX
 Referenced in 18 articles
[sw11674]
 general theorem proving system for propositional modal logics, called TABLEAUX. The main feature...

leanTAP
 Referenced in 41 articles
[sw09985]
 modal logics T, K4 and S4. The paper is restricted to the propositional case ... extended to the case of quantified modal logics as long as the Barcan formula...

LWB
 Referenced in 3 articles
[sw01820]
 Relations between propositional normal modal logics: An overview. In this short paper the authors give ... overview of the most common propositional normal modal logics by first providing a catalogue ... relationships between the logics; the equivalence between multiple axiomatizations of a logic is established ... theorem prover for propositional modal and other nonclassical logics. A pleasant side effect of their...

Concurrency Workbench
 Referenced in 12 articles
[sw14749]
 equivalences and preorders; define propositions in a powerful modal logic and check whether a given...

embed_modal
 Referenced in 4 articles
[sw28304]
 accomplish the most widely applicable modal logic theorem prover available to date, i.e. no other ... prover covers more variants of propositional and quantified modal logics. Despite this generality, our approach...

leanK
 Referenced in 1 article
[sw28630]
 free variable tableau calculus for propositional modal logics. leanK 2.0 includes additional search space restrictions...

MODPROF
 Referenced in 2 articles
[sw21543]
 prover and model finder for propositional and modal logic K. MODPROF is based on labelled...

CardKt
 Referenced in 1 article
[sw01599]
 perform automated deduction in propositional multimodal logics on a Java smart card. The tight...

MNiBLoS
 Referenced in 2 articles
[sw32318]
 universes), restricting the modal structures to the finite ones. At the propositional level, the solver ... best known infinitelyvalued fuzzy logics (including BL, Łukasiewicz, Gödel ... product logics), and with all the continuous tnorm based logics that can be finitely ... terms of the previous ones; concerning the modal expansion, mNiBLoS imposes no boundary...

Coq
 Referenced in 1913 articles
[sw00161]
 Coq is a formal proof management system. It...

Isabelle
 Referenced in 721 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

Mathematica
 Referenced in 6458 articles
[sw00554]
 Almost any workflow involves computing results, and that...

MiniSat
 Referenced in 584 articles
[sw00577]
 An extensible SATsolver. MiniSat is a minimalistic...

SETHEO
 Referenced in 122 articles
[sw00707]
 SETHEO: A highperformance theorem prover. The paper...

RelView
 Referenced in 102 articles
[sw00798]
 The RelViewSystem is an interactive tool for...

SCIP
 Referenced in 558 articles
[sw01091]
 SCIP is currently one of the fastest non...

KRIPKE
 Referenced in 8 articles
[sw01162]
 The relevant logics E, R and N R...

PRISM
 Referenced in 454 articles
[sw01186]
 PRISM: Probabilistic symbolic model checker. In this paper...