Computational logic
This article needs additional citations for verification. (April 2015) (Learn how and when to remove this template message)

This article or section appears to contradict itself.
(April 2015)

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".
The term “Computational Logic” came to prominence with the founding of the ACM Transactions on Computational Logic.^{[1]} However, the term was apparently introduced by J.A. Robinson in a 1970 paper in the Proceedings of the Sixth Annual Machine Intelligence Workshop, Edinburgh, 1970, entitled "Computational Logic: The Unification Computation" (Machine Intelligence 6:6372, Edinburgh University Press, 1971). The expression is used in the second paragraph with a footnote claiming that *computational logic* (the emphasis is in the paper) is "surely a better phrase than 'theorem proving', for the branch of artificial intelligence which deals with how to make machines do deduction efficiently". This sounds like coining the term; no reference to a previous use is mentioned. In 1972 the Metamathematics Unit at the University of Edinburgh was renamed “The Department of Computational Logic” in the School of Artificial Intelligence.^{[2]} 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 a company Computational Logic Inc. of the same name.
The term “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 coordinator of the Basic Research Project CompulogII, reused and generalized the term when he founded the ACM Transactions on Computational Logic in 2000 and became its first EditorinChief.
References
 ^ http://tocl.acm.org official website of ACM Transactions on Computational Logic
 ^ http://homepages.inf.ed.ac.uk/bundy/ Professor Alan Bundy's website
Further reading
 Dov M. Gabbay, Jörg H. Siekmann, John Woods, eds. (2014). Handbook of the History of Logic, Volume 9: Computational Logic. Elsevier. ISBN 9780080930671.