
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 firstorder rewrite systems...

GoodDyson
 Referenced in 10 articles
[sw06643]
 algorithm, which automatically conjectures, and then automatically proves, closedform 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. Counterexampledriven 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 pointset 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 nonlinear 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...