• Coq

  • Referenced in 1784 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 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 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 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 higher-order ... 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 run-time. 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 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 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 UNITY-based 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 well-typedness and proof obligations. Multilingual grammars, where one abstract syntax ... syntax trees are constructed in an interactive editor similar to proof editors based...