• Nominal Isabelle

  • Referenced in 76 articles [sw12055]
  • Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about programming language calculi involving ... establishes automatically the reasoning infrastructure for α-equated terms. We also prove strong induction principles...
  • Stranger

  • Referenced in 17 articles [sw09152]
  • take during program execution. Stranger can automatically (1) prove that an application is free from...
  • Tsukuba

  • Referenced in 10 articles [sw10116]
  • Tool. We present a tool for automatically proving termination of first-order rewrite systems...
  • GoodDyson

  • Referenced in 10 articles [sw06643]
  • algorithm, which automatically conjectures, and then automatically proves, closed-form expressions extending...
  • Tac

  • Referenced in 7 articles [sw09455]
  • Focused inductive theorem proving. Focused proof systems provide means for reducing and structuring ... illustrate how it is capable of automatically proving many theorems using induction and coinduction. Since ... automatic proof procedure is structured using focused proofs, its behavior is often rather easy ... with several examples of proved theorems, some achieved entirely automatically and others achieved with user...
  • SymbolicData

  • Referenced in 29 articles [sw04621]
  • different geometry theorem proving approaches and provers. To automatize such tests it is desirable...
  • TkWinHOL

  • Referenced in 8 articles [sw00968]
  • correctness of each transformation step is proved automatically by the HOL system. The interface...
  • Zapato

  • Referenced in 11 articles [sw25425]
  • zapato: Automatic theorem proving for predicate abstraction refinement. Counterexample-driven abstraction refinement is an automatic...
  • DET

  • Referenced in 7 articles [sw19265]
  • automatically conjectured, and then rigorously automatically proved, once we suspect that they belong...
  • LNgen

  • Referenced in 7 articles [sw10111]
  • sound and complete, with LNgen automatically proving many of the key lemmas. We prove...
  • Analytica

  • Referenced in 33 articles [sw10478]
  • theorem prover for Mathematica. Analytica is an automatic theorem prover for theorems in elementary analysis ... system to prove theorems that are beyond the scope of previous automatic theorem provers...
  • MUSCADET

  • Referenced in 10 articles [sw06859]
  • MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics. The author presents ... reduction, the knowledge base is adapted to prove theorems in point-set topology and topological ... spaces. The main ideas are exemplified by automatic proofs of some elementary facts on topological...
  • GEOTHER 1.1

  • Referenced in 32 articles [sw02842]
  • manipulate and prove the theorem. From the specification, GEOTHER can automatically assign coordinates to each ... dragging, and saved as PostScript files; prove the theorem using any of the five algebraic...
  • jStar

  • Referenced in 32 articles [sw11261]
  • automatic verification system, called jStar, which combines theorem proving and abstract interpretation techniques. We demonstrate...
  • Reveal

  • Referenced in 22 articles [sw00801]
  • designs with wide datapaths. Reveal performs automatic datapath abstraction yielding an approximation of the original ... approximation proves to be too coarse, it is automatically refined based on the spurious counterexample...
  • HSF

  • Referenced in 12 articles [sw09937]
  • finds auxiliary assertions required for proving software properties automatically...
  • Stabhyli

  • Referenced in 5 articles [sw20122]
  • present Stabhyli, a tool that automatically proves stability of non-linear hybrid systems. Hybrid systems ... reaction. We have implemented a tool to automatically derive a certificate of stability...
  • FLAGTOOL

  • Referenced in 5 articles [sw17626]
  • FLAGTOOL is a computer program for proving automatically theorems about the combinatorial structure of polytopes...
  • AI2

  • Referenced in 5 articles [sw40547]
  • Based on overapproximation, AI 2 can automatically prove safety properties (e.g., robustness) of realistic neural...