
Coq
 Referenced in 1784 articles
[sw00161]
 semiinteractive development of machinechecked proofs. Typical applications include the formalization of programming languages ... formalization of the 4 color theorem or constructive mathematics at Nijmegen) and teaching...

ETPS
 Referenced in 153 articles
[sw06302]
 proofs, translating these into natural deduction proofs, constructing natural deduction proofs, translating natural deduction proofs ... which do not contain cuts into expansion proofs, and solving unification problems in higherorder ... formula editor which facilitates constructing new formulas from others already known ... interactive facilities of TPS for constructing natural deduction proofs have been used under the name...

Pesca
 Referenced in 129 articles
[sw13664]
 program that helps in the construction of proofs in sequent calculus. It works both ... automatic theorem prover. Proofs constructed in Pesca can both be seen on the terminal...

TPS
 Referenced in 71 articles
[sw00973]
 proofs, translating these into natural deduction proofs, constructing natural deduction proofs, translating natural deduction proofs ... which do not contain cuts into expansion proofs, and solving unification problems in higherorder ... formula editor which facilitates constructing new formulas from others already known...

MPTP 0.2
 Referenced in 44 articles
[sw02589]
 translating of a number of Mizar proof constructs into the TPTP formalism. The proofs using...

Find
 Referenced in 82 articles
[sw21614]
 Proof of a program: Find. A proof is given of the correctness of the algorithm ... systematic technique is described for constructing the program proof during the process of coding...

Agda
 Referenced in 182 articles
[sw09689]
 checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics ... Löf. It has many similarities with other proof assistants based on dependent types, such...

REVE
 Referenced in 68 articles
[sw28907]
 emphasis is placed on mechanization of termination proof. Indeed, REVE ... recursive decomposition ordering which constructs the termination proof step by step from the presentation...

Analytica
 Referenced in 31 articles
[sw10478]
 main techniques that it uses to construct proofs. We have tried to make the paper...

Hyperproof
 Referenced in 24 articles
[sw22172]
 principles of analytical reasoning and proof construction, consisting of a text and a Macintosh software ... focus on the information content of proofs rather than the syntactic structure of sentences...

Waldmeister
 Referenced in 44 articles
[sw19568]
 Within that scope, a complete proof object is constructed at runtime. Read more about...

LEGO
 Referenced in 107 articles
[sw09685]
 LEGO is an interactive proof development system (proof assistant) designed and implemented by Randy Pollack ... Edinburgh Logical Framework (LF), the Calculus of Constructions (CC), the Generalized Calculus of Constructions ... LEGO is a powerful tool for interactive proof development in the natural deduction style...

Tecton
 Referenced in 9 articles
[sw28905]
 system is an experimental tool for constructing proofs of firstorder logic formulas ... designed to make interactive proof construction easier than with previous proof tools, by maintaining multiple...

JFLAP
 Referenced in 12 articles
[sw10334]
 JFLAP allows one to experiment with construction proofs from one form to another, such...

GeoThms
 Referenced in 24 articles
[sw06216]
 repository of geometrical constructions, figures and proofs. The GeoThms users can easily use/browse through existing ... system with a growing body of geometrical constructions and formally proven geometrical theorems. We believe...

UNITY
 Referenced in 184 articles
[sw13461]
 UNITY  a computational model, specification language and proof system defined by Chandy and Misra ... describe a UNITYbased methodology for the construction, analysis and execution of simulation models...

Mace4
 Referenced in 202 articles
[sw06905]
 formulas over the domain are constructed. The result is a set of ground clauses with ... theorem provers, with the prover searching for proofs and Mace4 looking for countermodels...

Lean
 Referenced in 30 articles
[sw15148]
 user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing...

HARP
 Referenced in 16 articles
[sw26323]
 Artificial Intelligence applications. Accordingly, HARP’s construction is influenced by the design goals of ‘naturalness ... kind of normal form, and combines a proof condensation procedure with explicitly ... represented, declaratively formulated heuristics to construct and communicate its proofs in a format congenial...

GF
 Referenced in 32 articles
[sw13667]
 semantic conditions, such as welltypedness and proof obligations. Multilingual grammars, where one abstract syntax ... syntax trees are constructed in an interactive editor similar to proof editors based...