• SQEMA

  • Referenced in 39 articles [sw03056]
  • order equivalents and proving canonicity of modal formulae, and thus established a very general correspondence ... most important of which employs a modal version of a result by Ackermann that enables ... existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that ... correctness for a large class of modal formulae containing an extension of the Sahlqvist formulae...
  • LoTREC

  • Referenced in 27 articles [sw07684]
  • counter-models and testing satisfiability of formulas in modal and description logics. This system...
  • CoLoSS

  • Referenced in 14 articles [sw07016]
  • Logic Satisfiability Solver, decides satisfiability of modal formulas in a generic and compositional ... polynomial space algorithm to decide satisfiability for modal logics that are amenable to coalgebric semantics...
  • leanTAP

  • Referenced in 41 articles [sw09985]
  • case of quantified modal logics as long as the Barcan formula is not assumed...
  • Cool

  • Referenced in 4 articles [sw11992]
  • decides the satisfiability of modal (and, more generally, hybrid) formulas with respect ... logical framework covering a wide range of modal logics, beyond relational semantics. The core...
  • SEQ.OPEN

  • Referenced in 1 article [sw00849]
  • using either regular expressions or modal $\mu $-calculus formulas, and verified efficiently on very large...
  • Concurrency Workbench

  • Referenced in 12 articles [sw14749]
  • preorders; define propositions in a powerful modal logic and check whether a given process satisfies ... process does or does not satisfy a formula; derive automatically logical formulae which distinguish nonequivalent...
  • Sibyl

  • Referenced in 6 articles [sw11995]
  • logic with binders, the converse and global modalities, transitivity assertions and relation hierarchies ... that the negation normal form of the formulae given in input do not contain...
  • KRIPKE

  • Referenced in 8 articles [sw01162]
  • modal S4 are decidable. This theorem was shown in [8] to be equivalent ... details of which see [9]). Given any formula A (in the appropriate vocabulary) the decision...
  • iCTRL

  • Referenced in 1 article [sw01473]
  • modal operators or certain modelling problems like one-to-one sentence–formula mapping. The CTRL/iCTRL...
  • MarCaSPiS

  • Referenced in 5 articles [sw06957]
  • addressing openendedness of SOC. Indeed, SoSL provides modal operators that can be used for specifying ... have developed ways for model-checking SoSL formulae against MarCaSPiS specifications by exploiting an existing...
  • Coq

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

  • Referenced in 3189 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • Gmsh

  • Referenced in 767 articles [sw00366]
  • Gmsh is a 3D finite element grid generator...
  • Isabelle

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

  • Referenced in 306 articles [sw00500]
  • LANCELOT. A Fortran package for large-scale nonlinear...
  • LAPACK

  • Referenced in 1702 articles [sw00503]
  • LAPACK is written in Fortran 90 and provides...
  • LEO-II

  • Referenced in 51 articles [sw00512]
  • LEO-II is a standalone, resolution-based higher...
  • LSQR

  • Referenced in 394 articles [sw00530]
  • Algorithm 583: LSQR: Sparse Linear Equations and Least...
  • Maple

  • Referenced in 5373 articles [sw00545]
  • The result of over 30 years of cutting...