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.
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.
Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by Dana Scott. Work on the LCF system introduced the general-purpose programming language ML to allow users to write theorem-proving tactics, supporting algebraic data types, parametric polymorphism, abstract data types, and exceptions.
ACL2 is a software system consisting of a programming language, an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for software and hardware verification. The input language and implementation of ACL2 are written in Common Lisp. ACL2 is free and open-source software.
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.
Vampire is an automatic theorem prover for first-order classical logic developed in the Department of Computer Science at the University of Manchester. Up to Version 3, it was developed by Andrei Voronkov together with Kryštof Hoder and previously with Alexandre Riazanov. Since Version 4, the development has involved a wider international team including Laura Kovacs, Giles Reger, and Martin Suda. Since 1999 it has won at least 53 trophies in the CADE ATP System Competition, the "world cup for theorem provers", including the most prestigious FOF division and the theory-reasoning TFA division.
Logic in computer science covers the overlap between the field of logic and that of computer science. The topic can essentially be divided into three main areas:
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.
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.
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 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.
The mutilated chessboard problem is a tiling puzzle posed by Max Black in 1946 that asks:
Suppose a standard 8×8 chessboard has two diagonally opposite corners removed, leaving 62 squares. Is it possible to place 31 dominoes of size 2×1 so as to cover all of these squares?
Harald Ganzinger was a German computer scientist who together with Leo Bachmair developed the superposition calculus, which is used in most of the state-of-the-art automated theorem provers for first-order logic.
David Alan Plaisted is a computer science professor at the University of North Carolina at Chapel Hill.
In mathematical logic and metalogic, a formal system is called complete with respect to a particular property if every formula having the property can be derived using that system, i.e. is one of its theorems; otherwise the system is said to be incomplete. The term "complete" is also used without qualification, with differing meanings depending on the context, mostly referring to the property of semantical validity. Intuitively, a system is called complete in this particular sense, if it can derive every formula that is true.
The Penrose–Lucas argument is a logical argument partially based on a theory developed by mathematician and logician Kurt Gödel. In 1931, he proved that every effectively generated theory capable of proving basic arithmetic either fails to be consistent or fails to be complete. Due to human ability to see the truth of formal system's Gödel sentences, it is argued that the human mind cannot be computed on a Turing Machine that works on Peano arithmetic because the latter can't see the truth value of its Gödel sentence, while human minds can. Mathematician Roger Penrose modified the argument in his first book on consciousness, The Emperor's New Mind (1989), where he used it to provide the basis of his theory of consciousness: orchestrated objective reduction.
Dafny is an imperative and functional compiled language that compiles to other programming languages, such as C#, Java, JavaScript, Go and Python. It supports formal specification through preconditions, postconditions, loop invariants, loop variants, termination specifications and read/write framing specifications. The language combines ideas from the functional and imperative paradigms; it includes support for object-oriented programming. Features include generic classes, dynamic allocation, inductive datatypes and a variation of separation logic known as implicit dynamic frames for reasoning about side effects. Dafny was created by Rustan Leino at Microsoft Research after his previous work on developing ESC/Modula-3, ESC/Java, and Spec#.
Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.
References
- ↑ "Max-Planck-Institut für Informatik - Automation of Logic: Spass". Spass-prover.org. 2010-05-28. Retrieved 2016-08-10.
- ↑ "Spass-Xdb". Cs.miami.edu. doi:10.1007/978-3-642-04617-9_36 . Retrieved 2016-08-10.
- ↑ David Stanovsky; Martin Suda; Geoff Sutcliffe. "SPASS-XDB goes Mathematical" (PDF). Karlin.mff.cuni.cz. Retrieved 2016-08-10.