
ZTree
 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 theoremprover for firstorder 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 higherorder logic interactively, automatically, or in a mixture of these ... solving unification problems in higherorder logic. It has a formula editor which facilitates constructing...

HOL Light
 Referenced in 310 articles
[sw06580]
 Light is an interactive proof assistant for classical higherorder 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 theoremprover for firstorder 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 higherorder logic interactively, automatically, or in a mixture of these ... solving unification problems in higherorder logic. It has a formula editor which facilitates constructing...

Isar
 Referenced in 145 articles
[sw04599]
 proof given by stateoftheart 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 metalogic implementation. Theories, theorems, proof procedures ... support a wide range of objectlogics. The current enduser 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 firstorder logic. Interactive theorem provers like pvs also make ... automatatheoretic techniques for firstorder 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 twolevel 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...