• Hazelnut

  • Referenced in 2 articles [sw22659]
  • Curry-Howard interpretation of contextual modal logic. Finally, we discuss how Hazelnut’s semantics lends...
  • Epistemic Logic

  • Referenced in 1 article [sw42014]
  • Epistemic_Logic: Epistemic Logic: Completeness of Modal Logics. This work is a formalization of epistemic ... logic with countably many agents. It includes proofs of soundness and completeness for the axiom ... proofs are based on the textbook ”Modal Logic” by Blackburn, de Rijke and Venema (Cambridge...
  • CardS4

  • Referenced in 1 article [sw01627]
  • implementation of a theorem prover for modal logic S4 that runs on a Java smart ... proof of principle” that non-trivial modal deduction is feasible even on current Java cards ... done to design the appropriate modal logics of “permission” and “obligations”. Such security concerns...
  • HyLoBan

  • Referenced in 1 article [sw17659]
  • topological interpretation of orthodox modal logic. We then examine two implemented proof methods. The first...
  • leanK

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

  • Referenced in 8 articles [sw01162]
  • relevant logics E, Ri, NRi and O R and the modal S4 are decidable. This ... decision procedure for each of these logics describes a way of recursively constructing...
  • MarCaSPiS

  • Referenced in 5 articles [sw06957]
  • resource oriented logic, which permits addressing openendedness of SOC. Indeed, SoSL provides modal operators that ... processes in a system at the logical level, i.e. without having to change the model...
  • PLM

  • Referenced in 3 articles [sw38031]
  • employs a modal relational type theory as logical foundation for which a representation in functional...
  • Molle

  • Referenced in 0 articles [sw05747]
  • cross-platform prover for modal logic. It exploits the modal semantic tableaux method. It features...
  • SOLOIST

  • Referenced in 1 article [sw16438]
  • first-order metric temporal logic, extended with new temporal modalities that support aggregate operators ... language can be reduced to linear temporal logic, paving the way for using SOLOIST with...
  • MetaGame

  • Referenced in 10 articles [sw00572]
  • cause of the problem. For branching time logics error diagnosis information can be given ... that computes and animates winning strategies for modal μ-calculus model checking games on finite...
  • CatLog3

  • Referenced in 4 articles [sw29641]
  • displacement calculus). extit{CatLog3} implements a logic including as primitive connectives the continuous (concatenation ... displacement calculus, additives, 1st order quantifiers, normal modalities, bracket modalities, and universal and existential subexponentials...
  • GI-log

  • Referenced in 3 articles [sw28522]
  • with graded introspection. This paper develops a logic programming language, GI-log, that extends answer ... programming language with a new graded modality Kω where ω is an interval satisfying...
  • VMC

  • Referenced in 5 articles [sw09745]
  • accepts a product family specified as a modal transition system, possibly with additional variability constraints ... action- and state-based branching-time temporal logic over products and families alike...
  • iCTRL

  • Referenced in 1 article [sw01473]
  • logic cannot cope with numerous natural language phenomena such as the large variety of modalities ... satisfactory interpretation of iterative application of modal operators or certain modelling problems like ... computer-aided textual data base generation and logical inference based information retrieval. CTRL/iCTRL applicability...
  • ANSYS

  • Referenced in 704 articles [sw00044]
  • ANSYS offers a comprehensive software suite that spans...
  • ASTRA

  • Referenced in 12 articles [sw00052]
  • Fault Tree Analysis (FTA) is a formalised deductive...
  • Coq

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

  • Referenced in 74 articles [sw00183]
  • Dafny is an imperative object-based language with...
  • GAP

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