Computational logic is the use of

logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from prem ...

to perform or reason about

computation Computation is any type of arithmetic or non-arithmetic calculation that follows a well-defined model (e.g., an algorithm). Mechanical or electronic devices (or, historically, people) that perform computations are known as ''computers''. An esp ...

. It bears a similar relationship to

computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...

and engineering as

mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of forma ...

bears to

mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...

and as

philosophical logic Understood in a narrow sense, philosophical logic is the area of logic that studies the application of logical methods to philosophical problems, often in the form of extended logical systems like modal logic. Some theorists conceive philosophical ...

bears to

philosophy Philosophy (from , ) is the systematized study of general and fundamental questions, such as those about existence, reason, knowledge, values, mind, and language. Such questions are often posed as problems to be studied or resolved. ...

. It is synonymous with "

logic in computer science 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: * Theoretical foundations and analysis * Use of computer technology to aid logicians ...

". The term “computational logic” came to prominence with the founding of the

ACM Transactions on Computational Logic ''ACM Transactions on Computational Logic'' (''ACM TOCL'') is a scientific journal that aims to disseminate the latest findings of note in the field of logic in computer science. It is published by the Association for Computing Machinery, a premier ...

in 2000. However, the term was introduced much earlier, by

J.A. Robinson John Alan Robinson (9 March 1930 – 5 August 2016) was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University. Alan Robinson's major contribution is to the foundations of automated theorem ...

in 1970. 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 The University of Edinburgh ( sco, University o Edinburgh, gd, Oilthigh Dhùn Èideann; abbreviated as ''Edin.'' in post-nominals) is a public research university based in Edinburgh, Scotland. Granted a royal charter by King James VI in 1 ...

was renamed “The Department of Computational Logic” in the School of Artificial Intelligence.http://homepages.inf.ed.ac.uk/bundy/ Professor Alan Bundy's website 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 In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...

and

automated reasoning 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 prog ...

. They also founded Computational Logic Inc. Computational logic has also come to be associated with

logic programming 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 pro ...

, 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

References

Further reading