Logic in Computer Science

Thierry Coquand Nov. 9, 2007

Logic in Computer Science

Mathematical Logic

Traditionally mathematical logic was developped by philosophers and mathematicians interested in foundations Logic plays a special role in computer science: it has been called “the calculus of computer science” Logic plays a similar role in computer science to that played by calculus in the physical sciences and traditional engineering disciplines. (M. Vardi, 2007)

1

Logic in Computer Science

Logic and Computer Science

“It is reasonable to hope that the relationship between computation and mathematical logic will be as fruitful in the next century as that between analysis and physics in the last.” (J. MacCarthy, 1961) Three systems propositional logic temporal logic predicate logic

2

Logic in Computer Science

History

The greeks (Aristotle) discovered the formal nature of logical reasonings All men are mortal All greeks are men. Hence all greeks are mortal We don’t need to understand what are “men”, “mortal”, “greeks” to recognise the validity of this inference

3

Logic in Computer Science

History

We can use symbols All A are B All B are C. Hence all A are C

4

Logic in Computer Science

History

This is like in algebra (symbols were introduced much later there) We can do the reasoning mechanically, without understanding the meaning of the symbols Leibniz had the idea of reducing reasoning (in various domains, for instance laws) to computation: “The only way to rectify our reasonings is to make them as tangible as those of the Mathematicians, so that we can ﬁnd our error at a glance, and when there are disputes among persons we can simply say: let us calculate.”

5

Logic in Computer Science

Propositional Logic

Propositional logic (Boole) provides precisely such a symbolic notation A → B, A ∧ B, A ∨ B, ¬A, A ↔ B Used extensively to automate reasoning in artiﬁcal intelligence

6

Logic in Computer...