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.
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.
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.
The Conference on Automated Deduction (CADE) is the premier academic conference on automated deduction and related fields. The first CADE was organized in 1974 at the Argonne National Laboratory near Chicago. Most CADE meetings have been held in Europe and the United States. However, conferences have been held all over the world. Since 1996, CADE has been held yearly. In 2001, CADE was, for the first time, merged into the International Joint Conference on Automated Reasoning (IJCAR). This has been repeated biannually since 2004.
The Herbrand Award for Distinguished Contributions to Automated Reasoning is an award given by the Conference on Automated Deduction (CADE), Inc., to honour persons or groups for important contributions to the field of automated deduction. The award is named after the French scientist Jacques Herbrand and given at most once per CADE or International Joint Conference on Automated Reasoning (IJCAR). It comes with a prize of US$1,000. Anyone can be nominated, the award is awarded after a vote among CADE trustees and former recipients, usually with input from the CADE/IJCAR programme committee.
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.
Alan Richard Bundy is a professor at the School of Informatics at the University of Edinburgh, known for his contributions to automated reasoning, especially to proof planning, the use of meta-level reasoning to guide proof search.
The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) is an annual international academic conference that deals with all aspects of automated reasoning with analytic tableaux. Periodically, it joins with CADE and TPHOLs into the International Joint Conference on Automated Reasoning (IJCAR).
Rewriting Techniques and Applications (RTA) is an annual international academic conference on the topic of rewriting. It covers all aspects of rewriting, including termination, equational reasoning, theorem proving, higher-order rewriting, unification and the lambda calculus. The conference consists of peer-reviewed papers with the proceedings published by Springer in the LNCS series until 2009, and since then in the LIPIcs series published by the Leibniz-Zentrum für Informatik. Several rewriting-related workshops are also affiliated with RTA.
Ian Robert Horrocks is a Professor of Computer Science at the University of Oxford in the UK and a Fellow of Oriel College, Oxford. His research focuses on knowledge representation and reasoning, particularly ontology languages, description logic and optimised tableaux decision procedures.
Drew McDermott is a former Professor of Computer Science at Yale University.
There are a number of competitions and prizes to promote research in artificial intelligence.
The International Workshop on First-Order Theorem Proving (FTP) is a scientific meeting of researchers interested in automated theorem proving for first-order logic and related fields. FTP workshops are less formal than many conferences, but more formal than most workshops. While FTP proceedings are published informally, most FTP workshops have resulted in a special issue of a recognized peer-reviewed academic journal.
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.
The Alan Turing Year, 2012, marked the celebration of the life and scientific influence of Alan Turing during the centenary of his birth on 23 June 1912. Turing had an important influence on computing, computer science, artificial intelligence, developmental biology, and the mathematical theory of computability and made important contributions to code-breaking during the Second World War. The Alan Turing Centenary Advisory committee (TCAC) was originally set up by Professor Barry Cooper
Ulrike M. Sattler is a Professor of Computer science in the information management group of the Department of Computer Science at the University of Manchester and a visiting professor at the University of Oslo.
Interactive Theorem Proving (ITP) is an annual international academic conference on the topic of automated theorem proving, proof assistants and related topics, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics.
The Vienna Summer of Logic was a scientific event in the summer of 2014, combining 12 major conferences and several workshops from the fields of mathematical logic, logic in computer science, and logic in artificial intelligence. The meetings took place from July 9 to 24, 2014, and attracted more than 2000 scientists and researchers.
Andrei Anatolievič Voronkov is a Professor of Formal methods in the Department of Computer Science at the University of Manchester.
