• HOL

  • Referenced in 557 articles [sw05492]
  • proved and proof tools implemented. Built-in decision procedures and theorem provers ... automatically establish many simple theorems. An Oracle mechanism gives access to external programs such...
  • TPTP

  • Referenced in 383 articles [sw04143]
  • library of test problems for automated theorem proving (ATP) systems. The TPTP supplies ... overview and a simple, unambiguous reference mechanism. A comprehensive list of references and other interesting...
  • UNITY

  • Referenced in 185 articles [sw13461]
  • coupled state transition systems. Mechanical methods for mapping the transition systems first into ... model should obey and prove them as theorems using the formal specification. The methodology...
  • LCF

  • Referenced in 157 articles [sw08360]
  • Edinburgh LCF. A mechanized logic of computation. From LCF to HOL: a short history ... invent the LCF-approach to theorem proving, but he also designed the ML programming language...
  • Walnut

  • Referenced in 24 articles [sw30122]
  • Automatic Theorem Proving in Walnut. Walnut is a software package that implements a mechanical decision...
  • Milawa

  • Referenced in 20 articles [sw09977]
  • mechanism. We have used the HOL4 theorem prover to formalize the logic of Milawa, prove...
  • MathScheme

  • Referenced in 9 articles [sw15109]
  • approach to mechanized mathematics in which computer algebra and computer theorem proving are merged without ... goal is to design and implement a mechanized mathematics system based on the formal framework...
  • OMRS

  • Referenced in 39 articles [sw03359]
  • Query and Manipulation Language) and OMRS (Open Mechanized Reasoning Systems). The claim is that ... communication of mathematical services in distributed theorem proving and symbolic computation environments...
  • GEOPAR

  • Referenced in 1 article [sw26046]
  • approach is shown that mechanically proves various theorems in plane geometry by recasting them...
  • ASASP

  • Referenced in 5 articles [sw06350]
  • problems-are mechanized by Satisfiability Modulo Theories solving and Automated Theorem Proving. asasp has been...
  • Omega-ANTS

  • Referenced in 9 articles [sw19626]
  • interactive and automated theorem proving. We present the $Omega$-ANTS theorem prover that is built ... agent-based command suggestion mechanism. The theorem prover inherits beneficial properties from the underlying suggestion...
  • reFLect

  • Referenced in 7 articles [sw22717]
  • functional language for hardware design and theorem proving. This paper introduces reFLect, a functional programming ... compiling reFLect programs using the same context mechanism...
  • SymProve3

  • Referenced in 2 articles [sw09242]
  • program for algebraic inequality decision. Mechanical inequality proving has been a hot and difficult point ... field of automated theorem proving. In this paper, we provide a mechanical algorithm for determining...
  • Kit

  • Referenced in 7 articles [sw22321]
  • proved. The problem is stated in the Boyer-Moore logic, and the proof is mechanically ... checked with the Boyer-Moore theorem prover...
  • WhyMP

  • Referenced in 1 article [sw36851]
  • mixture of mechanically checked handwritten proofs and automated theorem proving. We have implemented and verified...
  • Vellvm

  • Referenced in 6 articles [sw13286]
  • that operate on it. Vellvm provides a mechanized formal semantics of LLVM’s intermediate representation ... interactive theorem prover. It includes multiple operational semantics and proves relations among them to facilitate...
  • Verified Prover

  • Referenced in 3 articles [sw28795]
  • Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic. Soundness and completeness ... system of first order logic are formally proved, building on James Margetson’s formalization...
  • Proofwatch

  • Referenced in 3 articles [sw28654]
  • conjecture. This mechanism has been used with the Otter and Prover9 theorem provers, both ... interactive formalizations and for human-assisted proving of open conjectures in small theories. In this...
  • STORM

  • Referenced in 1 article [sw23070]
  • mechanism of discrimination nets, often used in non-AC theorem proving...
  • Speedith

  • Referenced in 6 articles [sw19455]
  • diagrammatic inference rules, and prove diagrammatic theorems. It is designed as a program that plugs ... into existing general purpose theorem provers. This allows for seamless formal verification of diagrammatic proof ... Speedith, the diagrammatic language, the automatic mechanism that draws the diagrams when inference rules...