
Hazelnut
 Referenced in 2 articles
[sw22659]
 CurryHoward 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 nontrivial 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]
 crossplatform prover for modal logic. It exploits the modal semantic tableaux method. It features...

SOLOIST
 Referenced in 1 article
[sw16438]
 firstorder 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...

GIlog
 Referenced in 3 articles
[sw28522]
 with graded introspection. This paper develops a logic programming language, GIlog, 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 statebased branchingtime 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 ... computeraided 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 objectbased language with...

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