• Matita

  • Referenced in 69 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 293 articles [sw06580]
  • Light: an overview. HOL Light is an interactive proof assistant for classical higher-order 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 51 articles [sw10060]
  • Interactive Verifier (KIV). KIV is an interactive theorem prover with a user definable object logic...
  • Abella

  • Referenced in 49 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...
  • Why3

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

  • Referenced in 120 articles [sw07047]
  • external first-order automatic theorem provers (ATPs) to discharge interactive proof obligations arising in Isabelle/HOL...
  • KeYmaera

  • Referenced in 41 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...
  • IsaPlanner

  • Referenced in 29 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 25 articles [sw09709]
  • help of various existing automated and interactive theorem provers. To keep verification conditions tractable...
  • 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...
  • CSP-prover

  • Referenced in 15 articles [sw11465]
  • Prover is an interactive theorem prover dedicated to refinement proofs within the process algebra...
  • HOL-Boogie

  • 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...
  • KAT-ML

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

  • Referenced in 11 articles [sw28573]
  • have formalised psi-calculi 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 156 articles [sw06302]
  • System. The former is an automated theorem-prover for first-order logic and type theory ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp...
  • 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...
  • LIRA

  • Referenced in 7 articles [sw21270]
  • fragments of first-order logic. Interactive theorem provers like pvs also make use of such...