Logic and Proof: 2019-2020
Lecturer | |
Degrees | Schedule S1(CS&P) — Computer Science and Philosophy |
Term | Trinity Term 2020 (16 lectures) |
Links |
Overview
Logic plays an important role in many disciplines, including Philosophy and Mathematics, but it is particularly central to Computer Science and sometimes referred to as the calculus of Computer Science. This course emphasises the computational aspects of logic, including applications to databases, constraint solving, programming and automated verification, among many others. We also highlight algorithmic problems in logic, such as SAT-solving, model checking and automated theorem proving, and round up the course with some basic concepts from model theory.
The course relates to a number of third-year and fourth-year options. Propositional and predicate logic are central to "Automata Logic and Games", "Computational Complexity", and "Knowledge Representation and Reasoning". They are also used extensively in "Computer-Aided Formal Verification" and "Probabilistic Model Checking".
Learning outcomes
At the end of the course students are expected to:
- Understand and be able to explain and illustrate the meaning of given logical formulas, to translate such formulas into English and vice-versa.
- Be able to use the resolution proof system in proposiitonal logic and in predicate logic.
- Be able to express and formalize in a logical language properties of models such as graphs, strings and transition systems, and be able to determine the truth or falsity of such formulas in a given model.
Synopsis
Propositional logic (7 Lectures).
- Introduction. History of mathematical logic in computer science.
- Syntax and semantics of propositional logic. The SAT problem. Translating constraint problems to SAT.
- Logical equivalence and algebraic reasoning. CNF and DNF.
- Polynomial-time algorithms: Horn formulas, 2-SAT, WalkSAT, and XOR-clauses.
- Resolution: soundness and refutation completeness.
- DPLL, clause learning, improvements, stochastic resolution.
- Compactness theorem.
First-order logic (9 Lectures).
- Signatures, structures and valuations.
- Examples: graphs, trees, strings, relational databases and number systems.
- Prenex normal form and Skolemisation.
- Herbrand models and ground resolution.
- Unification and resolution for predicate logic
- Undecidability of satisfiability.
- Logical theories, quantifier elimination
- Automatic structures.
- Ehrenfeucht-Fraisse games.
Syllabus
- Syntax of propositional logic. Truth tables.
- Horn-SAT and 2-SAT.
- Resolution. DPLL procedure.
- Compactness theorem.
- Syntax and semantics of first-order logic.
- Prenex normal form and Skolemisation.
- Herbrand models and ground resolution.
- Unification and resolution for predicate logic.
- Undecidability of satisfiability for first-order logic.
- Decidable theories, including linear arithmetic.
- Automatic structures.
- Ehrenfeucht-Fraisse games.
Reading list
Primary text:
- Logic for Computer Scientists. Uwe Schoning. Modern Birkäuser Classics, Reprint of the 1989 edition.
Secondary texts:
- Logic in computer science: modelling and reasoning about systems, 2nd edition, by M. Huth and M. Ryan. Cambridge University Press, 2004.
- Mathematical Logic for Computer Science, 3rd edition, by M. Ben-Ari. Springer, 2012.
- Handbook of Practical Logic and Automated Reasoning, by J. Harrison. Cambridge University Press, 2009.
Further literature:
- Gödel, Escher, Bach: an Eternal Golden Braid, by D. Hofstadter. Basic Books, 1979.
- Logicomix: An Epic Search for Truth, by A. Doxiadis and C. Papadimitriou. Bloomsbury Publishing PLC, 2009.