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.
Stephen Arthur Cook, is an American-Canadian computer scientist and mathematician who has made major contributions to the fields of complexity theory and proof complexity. He is a university professor at the University of Toronto, Department of Computer Science and Department of Mathematics.
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.
Metamathematics is the study of mathematics itself using mathematical methods. This study produces metatheories, which are mathematical theories about other mathematical theories. Emphasis on metamathematics owes itself to David Hilbert's attempt to secure the foundations of mathematics in the early part of the 20th century. Metamathematics provides "a rigorous mathematical technique for investigating a great variety of foundation problems for mathematics and logic". An important feature of metamathematics is its emphasis on differentiating between reasoning from inside a system and from outside a system. An informal illustration of this is categorizing the proposition "2+2=4" as belonging to mathematics while categorizing the proposition "'2+2=4' is valid" as belonging to metamathematics.
Thoralf Albert Skolem was a Norwegian mathematician who worked in mathematical logic and set theory.
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.
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 (SB) 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.
Lennart Axel Edvard Carleson is a Swedish mathematician, known as a leader in the field of harmonic analysis. One of his most noted accomplishments is his proof of Lusin's conjecture. He was awarded the Abel Prize in 2006 for "his profound and seminal contributions to harmonic analysis and the theory of smooth dynamical systems."
The Prototype Verification System (PVS) is a specification language integrated with support tools and an automated theorem prover, developed at the Computer Science Laboratory of SRI International in Menlo Park, California.
John Rushby is a British computer scientist now based in the United States and working for SRI International. He previously taught and did research for Manchester University and later Newcastle University.
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.
In computational complexity theory, the PCP theorem states that every decision problem in the NP complexity class has probabilistically checkable proofs of constant query complexity and logarithmic randomness complexity.
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.
Michael Fredric Sipser is an American theoretical computer scientist who has made early contributions to computational complexity theory. He is a professor of Applied Mathematics and was the Dean of Science at the Massachusetts Institute of Technology.
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.
Nqthm is a theorem prover sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2.
Richard Jay Waldinger is a computer science researcher at SRI International's Artificial Intelligence Center whose interests focus on the application of automated deductive reasoning to problems in software engineering and artificial intelligence.
David Alan Plaisted is a computer science professor at the University of North Carolina at Chapel Hill.
Sanjeev Arora is an Indian American theoretical computer scientist who is best known for his work on probabilistically checkable proofs and, in particular, the PCP theorem. He is currently the Charles C. Fitzmorris Professor of Computer Science at Princeton University, and his research interests include computational complexity theory, uses of randomness in computation, probabilistically checkable proofs, computing approximate solutions to NP-hard problems, geometric embeddings of metric spaces, and theoretical machine learning.
Grigore Roșu is a computer science professor at the University of Illinois at Urbana-Champaign and a researcher in the Information Trust Institute. He is known for his contributions in runtime verification, K framework, matching logic, and automated coinduction.
References
- 1 2 3 4 "Natarajan Shankar". Federated Logic Conference 2002. Retrieved 2012-03-11.
- ↑ "Metamathematics, Machines, and Goedel's Proof". SRI International . Retrieved 2012-03-11.
- 1 2 "SRI Fellows". SRI International . Retrieved 2012-03-11.
