• ARA

  • Referenced in 5 articles [sw08504]
  • System description: ARA -- an automatic theorem prover for relation algebras. ARA is an automatic theorem...
  • E-SETHEO

  • Referenced in 19 articles [sw07141]
  • domain. We present the theorem prover e-SETHEO, which automatically handles training data management, strategy...
  • EasyCrypt

  • Referenced in 33 articles [sw09738]
  • checked automatically using off-the-shelf SMT solvers and automated theorem provers, and then compiled...
  • Denali

  • Referenced in 4 articles [sw21711]
  • code generator that uses an automatic theorem prover to produce very high-quality (in fact...
  • IsaPlanner

  • Referenced in 30 articles [sw02047]
  • proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques ... used to conjecture and prove theorems automatically. The system provides an interactive tracing tool that ... based on the Isabelle theorem prover and the Isar language. The main proof technique written...
  • Nominal Isabelle

  • Referenced in 76 articles [sw12055]
  • definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about ... definitions of α-equivalence and establishes automatically the reasoning infrastructure for α-equated terms...
  • Zipperposition

  • Referenced in 3 articles [sw32251]
  • zipperposition: An automatic theorem prover in OCaml for typed higher-order logic with equality, datatypes...
  • GHC

  • Referenced in 43 articles [sw23765]
  • lost the completeness as a theorem prover deliberately, not as a result of compromise. Nevertheless ... Horn- clause programs. We showed how to automatically compile a Horn-clause program for exhaustive...
  • GeoView

  • Referenced in 9 articles [sw12328]
  • verified with Coq theorem prover. A dynamic figure is automatically associated to mathematical formulas...
  • KeYmaera

  • Referenced in 44 articles [sw03709]
  • automated and interactive theorem prover for a natural specification and verification logic for hybrid systems ... generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification...
  • Electronic Geometry Textbook

  • Referenced in 8 articles [sw08745]
  • users to create geometry textbooks with automatic checking, in real time, of the consistency ... textbook. By integrating an external geometric theorem prover and an external dynamic geometry software package ... system offers the facilities for automatically proving theorems and generating dynamic figures in the created...
  • ETPS

  • Referenced in 160 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 ... extent under Windows. Potential applications of automated theorem proving include hardware and software verification, partial ... used to prove theorems of first- and higher-order logic interactively, automatically...
  • SCC

  • Referenced in 11 articles [sw09809]
  • inductive theorem prover (ITP) that is used as a backend to try to automatically discharge...
  • Poitin

  • Referenced in 1 article [sw07544]
  • conjectures We describe a new fully automatic theorem prover called Poitín which makes...
  • HipSpec

  • Referenced in 14 articles [sw07736]
  • inductive theorem proving. HipSpec automatically generates a set of equational theorems about the available recursive ... HipSpec compares favourably to other inductive theorem provers and theory exploration systems...
  • TPS

  • Referenced in 73 articles [sw00973]
  • 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 ... extent under Windows. Potential applications of automated theorem proving include hardware and software verification, partial ... used to prove theorems of first- and higher-order logic interactively, automatically...
  • Pecan

  • Referenced in 1 article [sw37887]
  • Pecan: An Automated Theorem Prover for Automatic Sequences using Büchi Automata. Pecan is an automated...
  • Darwin

  • Referenced in 26 articles [sw04175]
  • Darwin is an automated theorem prover for first order clausal logic. It accepts problems formulated ... version of the calculus, it is instead automatically axiomatized for a given problem. Darwin...
  • PARTHENON

  • Referenced in 8 articles [sw25434]
  • elimination procedure was chosen for the theorem prover. The model elimination procedure is fully described ... role of parallelism in automatic theorem proving for future research...