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.
The Max Planck Institute for Informatics is a research institute in computer science with a focus on algorithms and their applications in a broad sense. It hosts fundamental research as well a research for various application domains.
J Strother Moore is a computer scientist. He is a co-developer of the Boyer–Moore string-search algorithm, Boyer–Moore majority vote algorithm, and the Boyer–Moore automated theorem prover, Nqthm. He made pioneering contributions to structure sharing including the piece table data structure and early logic programming. An example of the workings of the Boyer–Moore string search algorithm is given in Moore's website. Moore received his Bachelor of Science (BS) in mathematics at Massachusetts Institute of Technology in 1970 and his Doctor of Philosophy (Ph.D.) in computational logic at the University of Edinburgh in Scotland in 1973.
The superposition calculus is a calculus for reasoning in equational logic. It was developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of (unfailing) Knuth–Bendix completion. It can be seen as a generalization of either resolution or unfailing completion. Like most first-order calculi, superposition tries to show the unsatisfiability of a set of first-order clauses, i.e. it performs proofs by refutation. Superposition is refutation complete—given unlimited resources and a fair derivation strategy, from any unsatisfiable clause set a contradiction will eventually be derived.
Lawrence Charles Paulson is an American computer scientist. He is a Professor of Computational Logic at the University of Cambridge Computer Laboratory and a Fellow of Clare College, Cambridge.
Ross A. Overbeek is an American computer scientist with a long tenure at the Argonne National Laboratory. He has made important contributions to mathematical logic and genomics, as well as programming, particularly in database theory and the programming language Prolog.
The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.
The Handbook of Automated Reasoning is a collection of survey articles on the field of automated reasoning. Published in June 2001 by MIT Press, it is edited by John Alan Robinson and Andrei Voronkov. Volume 1 describes methods for classical logic, first-order logic with equality and other theories, and induction. Volume 2 covers higher-order, non-classical and other kinds of logic.
John Alan Robinson was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University.
David Alan Plaisted is a computer science professor at the University of North Carolina at Chapel Hill.
Kurt Mehlhorn is a German theoretical computer scientist. He has been a vice president of the Max Planck Society and is director of the Max Planck Institute for Computer Science.
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.
Leonhard Wolfgang Bibel is a German computer scientist, mathematician and Professor emeritus at the Department of Computer Science of the Technische Universität Darmstadt. He was one of the founders of the research area of artificial intelligence in Germany and Europe and has been named as one of the ten most important researchers in German artificial intelligence history by the Gesellschaft für Informatik. Bibel established the necessary institutions, conferences and scientific journals and promoted the necessary research programs to establish the field of artificial intelligence.
Thomas Henzinger is an Austrian computer scientist, researcher, and former president of the Institute of Science and Technology, Austria.
In mathematics and theoretical computer science, a set constraint is an equation or an inequation between sets of terms. Similar to systems of (in)equations between numbers, methods are studied for solving systems of set constraints. Different approaches admit different operators on sets and different (in)equation relations between set expressions.
Naveen Garg is a Professor of Computer Science in Indian Institute of Technology Delhi, specializing in algorithms and complexity in theoretical computer science. He was awarded the Shanti Swarup Bhatnagar Prize for Science and Technology, India's highest prize for excellence in science, mathematics and technology, in the mathematical sciences category in the year 2016. Naveen Garg's contributions are primarily in the design and analysis of approximation algorithms for NP-hard combinatorial optimization problems arising in network design, scheduling, routing, facility location etc.
Michael Backes is a German professor of computer science. He is the founding director and CEO of the CISPA Helmholtz Center for Information Security. He is known for his work on formal methods, cryptography and privacy-enhancing technologies.
Bernt Schiele is a German computer scientist. He is Max Planck Director at the Max Planck Institute for Informatics and professor at Saarland University. He is known for his work in the field of computer vision and perceptual computing.
Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.
