• KL-ONE

  • Referenced in 40 articles [sw28891]
  • related to propositional modal logics and logics of programs (such as propositional dynamic logic ... applications, most description logics differ significantly from run-of-the-mill modal and program logics...
  • ModLeanTAP

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

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

  • Referenced in 38 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 3 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 multi-modal 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 infinitely-valued fuzzy logics (including BL, Łukasiewicz, Gödel ... product logics), and with all the continuous t-norm based logics that can be finitely ... terms of the previous ones; concerning the modal expansion, mNiBLoS imposes no boundary...
  • Coq

  • Referenced in 1818 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Isabelle

  • Referenced in 617 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Mathematica

  • Referenced in 6041 articles [sw00554]
  • Almost any workflow involves computing results, and that...
  • MiniSat

  • Referenced in 541 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • SETHEO

  • Referenced in 119 articles [sw00707]
  • SETHEO: A high-performance theorem prover. The paper...
  • RelView

  • Referenced in 101 articles [sw00798]
  • The RelView-System is an interactive tool for...
  • SCIP

  • Referenced in 476 articles [sw01091]
  • SCIP is currently one of the fastest non...
  • PRISM

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