- Referenced in 594 articles
- implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems...
- Referenced in 634 articles
- integrated with support tools and a theorem prover. It is intended to capture the state...
- Referenced in 606 articles
- high-performance theorem prover being developed at Microsoft Research.Z3 supports linear real and integer arithmetic...
- Referenced in 401 articles
- TPTP (Thousands of Problems for Theorem Provers) is a library of test problems for automated...
E Theorem Prover
- Referenced in 206 articles
- Brainiac Theorem Prover: E is a theorem prover for full first-order logic with equality...
- Referenced in 310 articles
- Mike Gordon’s original HOL system. Theorem provers in this family use a version...
- Referenced in 151 articles
- truly important changes to the theorem prover since 1979 are the integration of a linear ... user to give hints to the theorem prover. The significant changes in the logic itself ... computational logic and its theorem prover” [J. Autom. Reasoning 4, No.2, 117-172 (1988)]. However ... changes to the logic and the theorem prover since the publication of the authors’ former...
- Referenced in 264 articles
- RV02,Vor05] is an automatic theorem prover for first-order classical logic. It consists ... result to the kernel. When a theorem is proved, the system produces a verifiable proof...
- Referenced in 228 articles
- useful complement to first-order theorem provers, with the prover searching for proofs and Mace4...
- Referenced in 198 articles
- Mace4: Prover9 is an automated theorem prover for first-order and equational logic, and Mace4...
- Referenced in 185 articles
- SPASS is an automated theorem prover for first-order logic with equality. So the input...
- Referenced in 122 articles
- SETHEO: A high-performance theorem prover. The paper deals with a theoretical background and practical ... interesting system SETHEO --- a theorem prover for first order logic. The system is based...
- Referenced in 166 articles
- language and theory. In contrast to theorem provers, the methods applied know about the underlying...
- Referenced in 164 articles
- proof editor and as an automatic theorem prover. Proofs constructed in Pesca can both...
- Referenced in 161 articles
- System. The former is an automated theorem-prover for first-order logic and type theory ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp...
- Referenced in 108 articles
- support the design of theorem provers, logic programming languages, constraints solvers and decision procedures ... support the design of theorem provers, logic programming languages, constraints solvers and decision procedures...
- Referenced in 97 articles
- SATCHMO: a theorem prover implemented in Prolog. The SATCHMO Theorem Prover...
- Referenced in 138 articles
- that harnesses external first-order automatic theorem provers (ATPs) to discharge interactive proof obligations arising...
- Referenced in 136 articles
- called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification...
- Referenced in 125 articles
- efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems...