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.
Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic programming language families include Prolog, answer set programming (ASP) and Datalog. In all of these languages, rules are written in the form of clauses:
Prolog is a logic programming language associated with artificial intelligence and computational linguistics.
Planner is a programming language designed by Carl Hewitt at MIT, and first published in 1969. First, subsets such as Micro-Planner and Pico-Planner were implemented, and then essentially the whole language was implemented as Popler by Julian Davies at the University of Edinburgh in the POP-2 programming language. Derivations such as QA4, Conniver, QLISP and Ether were important tools in artificial intelligence research in the 1970s, which influenced commercial developments such as KEE and ART.
Computer science is the study of the theoretical foundations of information and computation and their implementation and application in computer systems. One well known subject classification system for computer science is the ACM Computing Classification System devised by the Association for Computing Machinery.
EQP, an abbreviation for equational prover, is an automated theorem proving program for equational logic, developed by the Mathematics and Computer Science Division of the Argonne National Laboratory. It was one of the provers used for solving a longstanding problem posed by Herbert Robbins, namely, whether all Robbins algebras are Boolean algebras.
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.
In mathematical logic and logic programming, a Horn clause is a logical formula of a particular rule-like form which gives it useful properties for use in logic programming, formal specification, and model theory. Horn clauses are named for the logician Alfred Horn, who first pointed out their significance in 1951.
Ehud Shapiro is a multi-disciplinary scientist, artist, entrepreneur and a Professor of Computer Science and Biology at the Weizmann Institute of Science. With international reputation, he made fundamental contributions to many scientific disciplines. Ehud was also an Internet pioneer, a successful Internet entrepreneur, and a pioneer and proponent of E-democracy. Ehud is the founder of the Ba Rock Band and conceived its original artistic program. He is a winner of two ERC Advanced Grants.
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.
Robert Anthony Kowalski is a logician and computer scientist, whose research is concerned with developing both human-oriented models of computing and computational models of human thinking. He has spent most of his career in the United Kingdom.
Automated reasoning is an area of cognitive science and metalogic 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 even philosophy.
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.
Robert Stephen Boyer is a retired professor of computer science, mathematics, and philosophy at The University of Texas at Austin. He and J Strother Moore invented the Boyer–Moore string search algorithm, a particularly efficient string searching algorithm, in 1977. He and Moore also collaborated on the Boyer–Moore automated theorem prover, Nqthm, in 1992. Following this, he worked with Moore, and Matt Kaufmann on another theorem prover called ACL2.
Computational logic is the use of logic to perform or reason about computation. It bears a similar relationship to computer science and engineering as mathematical logic bears to mathematics and as philosophical logic bears to philosophy. It is synonymous with "logic in computer science".
John Alan Robinson was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University.
Larry Wos is an American mathematician, a researcher in the Mathematics and Computer Science Division of Argonne National Laboratory.
In information technology a reasoning system is a software system that generates conclusions from available knowledge using logical techniques such as deduction and induction. Reasoning systems play an important role in the implementation of artificial intelligence and knowledge-based systems.
Nikos Kyrpides is an American bioscientist of Greek descent who has worked on the origins of life, information processing, bioinformatics, microbiology, metagenomics and microbiome data science. He is a senior staff scientist at the Berkeley National Laboratory, head of the Prokaryote Super Program and leads the Microbiome Data Science program at the US Department of Energy Joint Genome Institute.
References
- 1 2 Leon Sterling (1990). The Practice of Prolog. MIT Press. ISBN 0-262-19301-9.
- ↑ D. W. Loveland (1984). "Automated Theorem Proving: A Quarter-Century Review". Contemporary Mathematics: Proceedings of the Special Session on Automatic Theorem Proving, 89th Annual Meeting of the American Mathematical Society, held in Denver, Colorado, January 5–9, 1983. 29. American Mathematical Society. ISBN 0-8218-5027-X.
The advocates of the resolution approach have by no means been quiescent during the 1970s. About 1972, the theorem prover of Wos, Robinson and Carson was replaced by one developed by Ross Overbeek. The system has continued to develop with contributions from S. Winker, E. Lusk, B. Smith and L. Wos. The system has been named AURA, for AUtomated Reasoning Assistant.... AURA is now viewed by its originators as a useful research tool for solving open problems subject to precise axiomatic formulations.
- ↑ "Speaker Information". The Institute of Bioinformatics. 2005. Archived from the original on 2007-08-10. Retrieved 2007-11-25.
- ↑ "Michael Fonstein, CEO of Integrated Genomics Inc., Wins KPMG Award". Integrated Genomics, Inc. November 20, 2000. Archived from the original on November 19, 2008. Retrieved 2007-11-25.
- ↑ "Fellowship for Interpretation of Genomes". Archived from the original on 2005-04-05. Retrieved 2007-11-24.
- ↑ "$18 million bioinformatics center to become weapon against deadly diseases". Argonne National Laboratory. September 3, 2004. Retrieved 2007-11-25.
