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.
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.
A non-monotonic logic is a formal logic whose conclusion relation is not monotonic. In other words, non-monotonic logics are devised to capture and represent defeasible inferences, i.e., a kind of inference in which reasoners draw tentative conclusions, enabling reasoners to retract their conclusion(s) based on further evidence. Most studied formal logics have a monotonic entailment relation, meaning that adding a formula to the hypotheses never produces a pruning of its set of conclusions. Intuitively, monotonicity indicates that learning a new piece of knowledge cannot reduce the set of what is known. Monotonic logics cannot handle various reasoning tasks such as reasoning by default, abductive reasoning, some important approaches to reasoning about knowledge, and similarly, belief revision.
The Journal of Artificial Intelligence Research (JAIR) is an open access peer-reviewed scientific journal covering research in all areas of artificial intelligence.
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.
Franz Baader is a German computer scientist at Dresden University of Technology.
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.
The Journal of Symbolic Computation is a peer-reviewed monthly scientific journal covering all aspects of symbolic computation published by Academic Press and then by Elsevier. It is targeted to both mathematicians and computer scientists. It was established in 1985 by Bruno Buchberger, who served as its editor until 1994.
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.
John Alan Robinson was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University.
The CADE ATP System Competition (CASC) is an annual competition of fully automated theorem provers for classical logic
Journal of Applied Non-Classical Logics is a peer-reviewed academic journal published by Taylor & Francis. It focusses on non-classical logic, in particular formal aspects, applications to artificial Intelligence and cognitive science, and theoretical computer science. The journal was established in 1991 by Luis Fariñas del Cerro, who was its editor-in-chief until 2014. He was succeeded in 2015 by Andreas Herzig.
Donald W. Loveland is a professor emeritus of computer science at Duke University who specializes in artificial intelligence. He is well known for the Davis–Putnam–Logemann–Loveland algorithm.
Tobias Nipkow is a German computer scientist.
Rina Dechter is a distinguished professor of computer science in the Donald Bren School of Information and Computer Sciences at the University of California, Irvine. Her research is on automated reasoning in artificial intelligence focusing on probabilistic and constraint-based reasoning. In 2013, she was elected a Fellow of the Association for Computing Machinery.
Andrei Anatolievič Voronkov is a Professor of Formal methods in the Department of Computer Science at the University of Manchester.
Michael John Wooldridge is a professor of computer science at the University of Oxford. His main research interests is in multi-agent systems, and in particular, in the computational theory aspects of rational action in systems composed of multiple self-interested agents. His work is characterised by the use of techniques from computational logic, game theory, and social choice theory.
Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.
Sylvie Thiébaux is a French-Australian computer scientist, whose research in artificial intelligence focuses on automated planning and scheduling, diagnosis, and automated reasoning under uncertainty. She is a professor of computer science at the Australian National University, and co-editor-in-chief of the journal Artificial Intelligence.
Dale Miller is an American computer scientist and author. He is a Director of Research at Inria Saclay and one of the designers of the λProlog programming language and the Abella interactive theorem prover.
