• Coq

  • Referenced in 1725 articles [sw00161]
  • semi-interactive development of machine-checked 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 151 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 higher-order ... 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 116 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 70 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 higher-order ... formula editor which facilitates constructing new formulas from others already known...
  • MPTP 0.2

  • Referenced in 43 articles [sw02589]
  • translating of a number of Mizar proof constructs into the TPTP formalism. The proofs using...
  • Find

  • Referenced in 80 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 170 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 23 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 43 articles [sw19568]
  • Within that scope, a complete proof object is constructed at run-time. Read more about...
  • LEGO

  • Referenced in 106 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 first-order 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 23 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 173 articles [sw13461]
  • UNITY -- a computational model, specification language and proof system defined by Chandy and Misra ... describe a UNITY-based methodology for the construction, analysis and execution of simulation models...
  • Mace4

  • Referenced in 193 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...
  • GF

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

  • Referenced in 15 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...
  • Lean

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