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 study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...

to perform or reason about

computation A computation is any type of arithmetic or non-arithmetic calculation that is well-defined. Common examples of computation are mathematical equation solving and the execution of computer algorithms. Mechanical or electronic devices (or, hist ...

. It bears a similar relationship to

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

and engineering as

mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...

bears to

mathematics Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...

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 philosophic ...

bears to

philosophy Philosophy ('love of wisdom' in Ancient Greek) is a systematic study of general and fundamental questions concerning topics like existence, reason, knowledge, Value (ethics and social sciences), value, mind, and language. It is a rational an ...

. It is an alternative term for "

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 ...

". Computational logic has also come to be associated with

logic programming Logic programming is a programming, database and knowledge representation paradigm based on formal logic. A logic program is a set of sentences in logical form, representing knowledge about some problem domain. Computation is performed by applyin ...

, 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. The term “computational logic” came to prominence with the founding of the ACM Transactions on Computational Logic in 2000. However, the term was introduced much earlier, by J.A. Robinson 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 (, ; abbreviated as ''Edin.'' in Post-nominal letters, post-nominals) is a Public university, public research university based in Edinburgh, Scotland. Founded by the City of Edinburgh Council, town council under th ...

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 Robert Stephen Boyer is an American retired professor of computer science, mathematics, and philosophy at University of Texas at Austin, The University of Texas at Austin. He and J Strother Moore invented the Boyer–Moore string-search algorit ...

and

J Strother Moore J Strother Moore (his first name is the alphabetic character "J" – not an abbreviated "J.") is an American computer scientist. He is a co-developer of the Boyer–Moore string-search algorithm, Boyer–Moore majority vote algorithm, and the Boy ...

, 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 a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal ver ...

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 progr ...

. They also founded Computational Logic Inc.

See also

References

Further reading