Related Research Articles
Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.
In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects.
Otter is an automated theorem prover developed by William McCune at Argonne National Laboratory in Illinois. Otter was the first widely distributed, high-performance theorem prover for first-order logic, and it pioneered a number of important implementation techniques. Otter is an acronym for Organized Techniques for Theorem-proving and Effective Research.
E is a high-performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem proving competitions. E is developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich, now at Baden-Württemberg Cooperative State University Stuttgart.
Paradox is a finite-domain model finder for pure first-order logic (FOL) with equality developed by Koen Lindström Claessen and Niklas Sörensson at the Chalmers University of Technology. It can a participate as part of an automated theorem proving system. The software is primarily written in the Haskell programming language. It is released under the terms of the GNU General Public License and is free.
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.
In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem.
In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.
The International Joint Conference on Automated Reasoning (IJCAR) is a series of conferences on the topics of automated reasoning, automated deduction, and related fields. It is organized semi-regularly as a merger of other meetings. IJCAR replaces those independent conferences in the years it takes place. The conference is organized by the organizers of the Conference on Automated Deduction (CADE), and CADE has always been one of the conferences partaking in IJCAR.
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.
In the computer science fields of knowledge engineering and ontology, the Sigma knowledge engineering environment (SigmaKEE) is an open source computer program for the development of formal ontologies. It is designed for use with the Suggested Upper Merged Ontology. It originally included only the Vampire theorem prover as its core deductive inference engine, but now allows use of many other provers that have participated in the CASC/CADE competitions.
SPASS is an automated theorem prover for first-order logic with equality developed at the Max Planck Institute for Computer Science and using the superposition calculus. The name originally stood for Synergetic Prover Augmenting Superposition with Sorts. The theorem-proving system is released under the FreeBSD license.
Geoff Sutcliffe is a US-based computer scientist working in the field of automated reasoning. He was born in the former British colony of Northern Rhodesia , grew up in South Africa, and earned his PhD in Australia. Sutcliffe currently works at the University of Miami, and is of both British and Australian nationality.
Christoph Walther is a German computer scientist, known for his contributions to automated theorem proving. He is Professor emeritus at Darmstadt University of Technology.
Charles Gregory Nelson was an American computer scientist.
Andrei Anatolievič Voronkov is a Professor of Formal methods in the Department of Computer Science at the University of Manchester.
TPTP is a freely available collection of problems for automated theorem proving. It is used to evaluate the efficacy of automated reasoning algorithms. Problems are expressed in a simple text-based format for first order logic or higher-order logic. TPTP is used as the source of some problems in CASC.
In computer science and mathematical logic, Cooperating Validity Checker (CVC) is a family of satisfiability modulo theories (SMT) solvers. The latest major versions of CVC are CVC4 and CVC5 ; earlier versions include CVC, CVC Lite, and CVC3. Both CVC4 and cvc5 support the SMT-LIB and TPTP input formats for solving SMT problems, and the SyGuS-IF format for program synthesis. Both CVC4 and cvc5 can output proofs that can be independently checked in the LFSC format, cvc5 additionally supports the Alethe and Lean 4 formats. cvc5 has bindings for C++, Python, and Java.
References
- ↑ Sutcliffe, Geoff (2011). "The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5". AI Communications. 24 (1): 75–89. doi:10.3233/AIC-2010-0483.
- ↑ Geoff Sutcliffe. "The CADE ATP System Competition". Archived from the original on 2009-03-02. Retrieved 2008-10-23.
- 1 2 Geoff Sutcliffe and Christian Suttner (2006). "The State of CASC". AI Communications. 19 (1): 35–48.
- ↑ Jeff Pelletier, Geoff Sutcliffe and Christian Suttner (2002). "The Development of CASC" (PDF). AI Communications. 15 (2–3): 79–90.
- ↑ Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). "SMT-COMP: Satisfiability Modulo Theories Competition" (PDF). Computer Aided Verification . Lecture Notes in Computer Science. 3576. Springer: 20–23. doi:10.1007/11513988_4. ISBN 978-3-540-27231-1.
- ↑ Matti, Järvisalo; Le Berre, Daniel; Roussel, Olivier; Simon, Laurent (2012). "The international SAT solver competitions". AI Magazine. 33 (1): 89–92. doi: 10.1609/aimag.v33i1.2395 .
- ↑ Massacci, Fabio; Donini, Francesco M. (2000). "Design and results of TANCS-2000 non-classical (modal) systems comparison". International Conference on Automated Reasoning with Analytic Tableaux and Related Methods . Lecture Notes in Computer Science. 1847. Springer: 52–56. CiteSeerX 10.1.1.385.6267 . doi:10.1007/10722086_4. ISBN 978-3-540-67697-3.
- ↑ McCune, William; Wos, Larry (1997). "Otter-the CADE-13 competition incarnations". Journal of Automated Reasoning . 18 (2): 211–220. doi:10.1023/A:1005843632307. S2CID 2481653.
- ↑ Moser, Max; Ibens, Ortrun; Letz, Reinhold; Steinbach, Joachim; Goller, Christoph; Schumann, Johann; Mayr, Klaus (1997). "Otter-the CADE-13 competition incarnations". Journal of Automated Reasoning. 18 (2): 237–246. doi:10.1023/A:1005808119103. S2CID 821198.