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.
Proof theory is a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of a given logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.
The QED manifesto was a proposal for a computer-based database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically.
The Suggested Upper Merged Ontology (SUMO) is an upper ontology intended as a foundation ontology for a variety of computer information processing systems. SUMO defines a hierarchy of classes and related rules and relationships. These are expressed in a version of the language SUO-KIF, a higher-order logic that has a LISP-like syntax, as well as the TPTP family of languages. A mapping from WordNet synsets to SUMO has been defined. Initially, SUMO was focused on meta-level concepts, and thereby would lead naturally to a categorization scheme for encyclopedias. It has now been considerably expanded to include a mid-level ontology and dozens of domain ontologies.
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.
Carew Arthur Meredith, usually cited as C. A. Meredith, was an influential Irish logician, who worked in Trinity College, Dublin from 1943 to 1964. His work on condensed detachment is influential in modern research.
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.
SNARK, , is a theorem prover for multi-sorted first-order logic intended for applications in artificial intelligence and software engineering, developed at SRI International.
There are a number of competitions and prizes to promote research in artificial intelligence.
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.
The CADE ATP System Competition (CASC) is a yearly competition of fully automated theorem provers for classical logic CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated Reasoning organized by the Association for Automated Reasoning. It has inspired similar competition in related fields, in particular the successful SMT-COMP competition for Satisfiability Modulo Theories, the SAT Competition for propositional reasoners, and the modal logic reasoning competition.
System on TPTP is an online interface to several automated theorem proving systems and other automated reasoning tools. It allows users to run the systems either on problems from the latest releases from the TPTP problem library or on user-supplied problems in the TPTP syntax.
In information technology a reasoning system is a software system that generates conclusions from available knowledge using logical techniques such as deduction and induction. Reasoning systems play an important role in the implementation of artificial intelligence and knowledge-based systems.
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.
Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.
