Computational logic

Last updated

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 an alternative rerm for "logic in computer science".

Contents

The term “computational logic” came to prominence with the founding of the ACM Transactions on Computational Logic in 2000. [1] However, the term was introduced much earlier, by J.A. Robinson in 1970. [2] The expression is used in the second paragraph with a footnote claiming that "computational logic" is "surely a better phrase than 'theorem proving', for the branch of artificial intelligence which deals with how to make machines do deduction efficiently".

In 1972 the Metamathematics Unit at the University of Edinburgh was renamed “The Department of Computational Logic” in the School of Artificial Intelligence. [3] The term was then used by Robert S. Boyer and J Strother Moore, who worked in the Department in the early 1970s, to describe their work on program verification and automated reasoning. They also founded Computational Logic Inc.

Computational logic has also come to be associated with logic programming, because much of the early work in logic programming in the early 1970s also took place in the Department of Computational Logic in Edinburgh. It was reused in the early 1990s to describe work on extensions of logic programming in the EU Basic Research Project "Compulog" and in the associated Network of Excellence. Krzysztof Apt, who was the co-ordinator of the Basic Research Project Compulog-II, reused and generalized the term when he founded the ACM Transactions on Computational Logic in 2000 and became its first Editor-in-Chief.

See also

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.

<span class="mw-page-title-main">Computer science</span> Study of computation

Computer science is the study of computation, information, and automation. Computer science spans theoretical disciplines to applied disciplines. Though more often considered an academic discipline, computer science is closely related to computer programming.

Knowledge representation and reasoning is the field of artificial intelligence (AI) dedicated to representing information about the world in a form that a computer system can use to solve complex tasks such as diagnosing a medical condition or having a dialog in a natural language. Knowledge representation incorporates findings from psychology about how humans solve problems, and represent knowledge in order to design formalisms that will make complex systems easier to design and build. Knowledge representation and reasoning also incorporates findings from logic to automate various kinds of reasoning.

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 Knowledge Engineering Environment (KEE) and Automated Reasoning Tool (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.

<span class="mw-page-title-main">Logic in computer science</span> Academic discipline

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:

<span class="mw-page-title-main">Robert Kowalski</span> British computer scientist (born 1941)

Robert Anthony Kowalski is an American-British 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.

Indeterminacy in concurrent computation is concerned with the effects of indeterminacy in concurrent computation. Computation is an area in which indeterminacy is becoming increasingly important because of the massive increase in concurrency due to networking and the advent of many-core computer architectures. These computer systems make use of arbiters which gives rise to indeterminacy.

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.

Dov M. Gabbay is an Israeli logician. He is Augustus De Morgan Professor Emeritus of Logic at the Group of Logic, Language and Computation, Department of Computer Science, King's College London.

<span class="mw-page-title-main">Woody Bledsoe</span> American mathematician and computer scientist

Woodrow Wilson "Woody" Bledsoe was an American mathematician, computer scientist, and prominent educator. He is one of the founders of artificial intelligence (AI), making early contributions in pattern recognition, facial recognition, and automated theorem proving. He continued to make significant contributions to AI throughout his long career. One of his influences was Frank Rosenblatt.

<span class="mw-page-title-main">Alan Bundy</span> British artificial intelligence researcher (born 1947)

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.

<span class="mw-page-title-main">John Alan Robinson</span> American computer scientist

John Alan Robinson was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University.

<span class="mw-page-title-main">Carl Hewitt</span> American computer scientist; Planner programming languagedesigner (1944-2022)

Carl Eddie Hewitt was an American computer scientist who designed the Planner programming language for automated planning and the actor model of concurrent computation, which have been influential in the development of logic, functional and object-oriented programming. Planner was the first programming language based on procedural plans invoked using pattern-directed invocation from assertions and goals. The actor model influenced the development of the Scheme programming language, the π-calculus, and served as an inspiration for several other programming languages.

Christoph Walther is a German computer scientist, known for his contributions to automated theorem proving. He is Professor emeritus at Darmstadt University of Technology.

Bernard Meltzer was a British computer scientist, who with Donald Michie was one of the main founders of research on artificial intelligence at the University of Edinburgh.

Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.

References

  1. http://tocl.acm.org official website of ACM Transactions on Computational Logic
  2. Robinson, J.A. (1970). "Computational Logic: The Unification Computation". In Meltzer, Bernard; Michie, Donald (eds.). Proceedings of the Sixth Annual Machine Intelligence Workshop. Machine Intelligence. Vol. 6. Edinburgh University Press (published 1971). pp. 63–72. ISBN   085224195X.
  3. http://homepages.inf.ed.ac.uk/bundy/ Professor Alan Bundy's website

Further reading