
Matita
 Referenced in 72 articles
[sw06140]
 pencil in italian) is an experimental, interactive theorem prover under development at the Computer Science ... University of Bologna. An interactive prover is a software tool aiding the development of formal ... mathematical definitions, executable algorithms and theorems cohexist, and an interactive environment keeping the current status...

HOL Light
 Referenced in 310 articles
[sw06580]
 Light: an overview. HOL Light is an interactive proof assistant for classical higherorder logic ... Mike Gordon’s original HOL system. Theorem provers in this family use a version ... both the implementation and interaction language; in HOL Light’s case this is Objective CAML...

KIV
 Referenced in 53 articles
[sw10060]
 Interactive Verifier (KIV). KIV is an interactive theorem prover with a user definable object logic...

Abella
 Referenced in 52 articles
[sw09461]
 Abella Interactive Theorem Prover (System Description). Abella [3] is an interactive system for reasoning about ... foundations of Abella, outlines the style of theorem proving that it supports and finally describes...

Sledgehammer
 Referenced in 138 articles
[sw07047]
 external firstorder automatic theorem provers (ATPs) to discharge interactive proof obligations arising in Isabelle/HOL...

KeYmaera
 Referenced in 48 articles
[sw03709]
 KeYmaera: A hybrid theorem prover for hybrid systems. KeYmaera is a hybrid verification tool ... technologies. It is an automated and interactive theorem prover for a natural specification and verification...

Why3
 Referenced in 136 articles
[sw04438]
 relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes...

IsaPlanner
 Referenced in 30 articles
[sw02047]
 framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding ... conjecture and prove theorems automatically. The system provides an interactive tracing tool that allows ... interact the proof planning attempt. (see the screenshot of IsaPlanner being used with Isabelle ... based on the Isabelle theorem prover and the Isar language. The main proof technique written...

WhyML
 Referenced in 28 articles
[sw09709]
 help of various existing automated and interactive theorem provers. To keep verification conditions tractable...

CSPprover
 Referenced in 17 articles
[sw11465]
 Prover is an interactive theorem prover dedicated to refinement proofs within the process algebra...

miz3
 Referenced in 11 articles
[sw18631]
 implemented on top of any procedural interactive theorem prover, regardless of its architecture and logical ... Light interactive theorem prover. The declarative language that this interface uses is a slight variant ... used for any interactive theorem prover regardles s of its logical foundations. The miz3 interface ... straightforward way to port proofs between interactive theorem provers...

HOLBoogie
 Referenced in 14 articles
[sw00409]
 annotations  are usually transferred to automated theorem provers such as Simplify or Z3. In this ... BoogieP, that combines Boogie with the interactive theorem prover Isabelle/HOL. In particular, we present specific...

GETFOL
 Referenced in 10 articles
[sw26307]
 GETFOL Interactive Theorem Prover. GETFOL is an interactive reasoning system running ... building intelligent systems, as an interactive theorem prover for first order logic...

KATML
 Referenced in 10 articles
[sw08506]
 interactive theorem prover for Kleene algebra with tests. We describe KATML, an implementation ... interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect...

Psicalculi
 Referenced in 11 articles
[sw28573]
 have formalised psicalculi in the interactive theorem prover Isabelle using its nominal datatype package...

GAPT
 Referenced in 9 articles
[sw22200]
 deduction. In contrast to automated and interactive theorem provers whose focus is the construction...

ETPS
 Referenced in 160 articles
[sw06302]
 System. The former is an automated theoremprover for firstorder logic and type theory ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp...

LIRA
 Referenced in 8 articles
[sw21270]
 fragments of firstorder logic. Interactive theorem provers like pvs also make use of such...

Dr.Doodle
 Referenced in 7 articles
[sw09975]
 paper presents the Dr.Doodle system, an interactive theorem prover that uses diagrammatic representations. The assumption...

LPTP
 Referenced in 7 articles
[sw01822]
 author. LPTP is an interactive theorem prover in which one can prove correctness properties...