• Z-Tree

  • Referenced in 659 articles [sw11707]
  • flexible both with respect to the logic of interaction and the visual representation, allowing...
  • ETPS

  • Referenced in 161 articles [sw06302]
  • automated theorem-prover for first-order logic and type theory. The latter ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... theorems of first- and higher-order logic interactively, automatically, or in a mixture of these ... solving unification problems in higher-order logic. It has a formula editor which facilitates constructing...
  • HOL Light

  • Referenced in 310 articles [sw06580]
  • Light is an interactive proof assistant for classical higher-order logic, intended as a clean ... both the implementation and interaction language; in HOL Light’s case this is Objective CAML ... clean and simple design and extremely small logical kernel. Despite this, it provides powerful proof...
  • TPS

  • Referenced in 75 articles [sw00973]
  • automated theorem-prover for first-order logic and type theory. The latter ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... theorems of first- and higher-order logic interactively, automatically, or in a mixture of these ... solving unification problems in higher-order logic. It has a formula editor which facilitates constructing...
  • Isar

  • Referenced in 145 articles [sw04599]
  • proof given by state-of-the-art interactive theorem proving systems and an appropriate level ... underlying logic, and integrates a broad range of automated proof methods. Interactive proof development ... tightly integrated into the Isabelle/Pure meta-logic implementation. Theories, theorems, proof procedures ... support a wide range of object-logics. The current end-user setup is mainly...
  • Reveal

  • Referenced in 22 articles [sw00801]
  • verify the correctness of control logic interactions. If the approximation proves to be too coarse...
  • Why3

  • Referenced in 136 articles [sw04438]
  • interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer...
  • PROMELA

  • Referenced in 30 articles [sw07635]
  • systems, and for expressing logical correctness requirements about such interactions. The model checker SPIN accepts...
  • LEGO

  • Referenced in 108 articles [sw09685]
  • LEGO is an interactive proof development system (proof assistant) designed and implemented by Randy Pollack ... implements various related type systems - the Edinburgh Logical Framework (LF), the Calculus of Constructions ... LEGO is a powerful tool for interactive proof development in the natural deduction style...
  • SCIFF

  • Referenced in 20 articles [sw20513]
  • Verifiable agent interaction in abductive logic programming: the SCIFF framework. SCIFF is a framework thought ... specify and verify interaction in open agent societies. The SCIFF language is equipped with ... semantics based on abductive logic programming; SCIFF’s operational component is a new abductive logic...
  • TRIPLE

  • Referenced in 21 articles [sw02460]
  • provided as modules that interact with a description logic classifier, e.g. FaCT, resulting...
  • KIV

  • Referenced in 53 articles [sw10060]
  • interactive theorem prover with a user definable object logic. The main applications rely...
  • KeYmaera

  • Referenced in 48 articles [sw03709]
  • automated and interactive theorem prover for a natural specification and verification logic for hybrid systems...
  • LIRA

  • Referenced in 8 articles [sw21270]
  • procedures for fragments of first-order logic. Interactive theorem provers like pvs also make ... automata-theoretic techniques for first-order logics with linear arithmetic, namely...
  • IMPS

  • Referenced in 52 articles [sw09143]
  • interactive mathematical proof system. IMPS is an interactive mathematical proof system intended as a general ... applying mathematics in a familiar fashion. The logic of IMPS is based on a version...
  • CESAR

  • Referenced in 161 articles [sw08510]
  • protocol, the use of CESAR, an interactive system for aiding the design of distributed applications ... formulas of a branching time logic, the temporal operators of which can be computed iteratively...
  • N3Logic

  • Referenced in 9 articles [sw02003]
  • N3Logic: A logical framework for the world wide web The Semantic Web drives toward ... interacting with logically interconnected data. Through knowledge models such as Resource Description Framework...
  • Abella

  • Referenced in 52 articles [sw09461]
  • Prover (System Description). Abella [3] is an interactive system for reasoning about aspects of object ... syntactic structure. Abella utilizes a two-level logic approach to specification and reasoning. One level...
  • miz3

  • Referenced in 11 articles [sw18631]
  • procedural interactive theorem prover, regardless of its architecture and logical foundations. To show the viability ... miz3 , on top of the HOL Light interactive theorem prover. The declarative language that this ... used for any interactive theorem prover regardles s of its logical foundations. The miz3 interface ... straightforward way to port proofs between interactive theorem provers...