COMP20142: Logic in Computer Science (2007-2008)
This course intends to build an understanding of fundamentals of (mathematical) logic as well as some of the applications of logic in modern computer science, including hardware verification, finite domain constraint satisfaction, and databases.
A student completing this course unit should:
Have a knowledge about basic reasoning (or satisfiability-checking) algorithms for propositional logic (A).
To understand BDDS (binary decision diagrams) as a data structure for compact representation of propositional formulas (A).
Have a knowledge about applications of propositional logic (such as finite domain constraint satisfaction and planning) and be able to apply it for solving hard combinatorial problems (B and C).
Have a knowledge of simple temporal logics (A).
Be able to specify properties of simple finite-state systems in temporal logics (B).
Be able to use first-order logic for knowledge representation (A).
To understand relations between logic and database query languages (A).
Assessment of Learning outcomesLearning outcomes (1), (2) and (6) are assesed both by examination and exercises. Learning outcomes (3), (4), (5) and (7) are assessed by examination.
Contribution to Programme Learning OutcomesA1, A2, A5, B1, C5 and C6.
Lectures 1-6. Propositional logic
Syntax and semantics. Validity and satisfiability. Satisfiability checking. Splitting and tableau-based algorithms for satisfiability checking. Binary decision diagrams. Propositional logic and finite-domain constraint satisfaction.
Lectures 7-12. Temporal logic
Syntax and semantics. Kripke structures. Specification of concurrent systems in temporal logic. Automatic verification of concurrent systems by model checking.
Lectures 13-18. First-order logic
Syntax and semantics. Reasoning in first-order logic.
Lectures 19-24. Logic in databases
Logic and database query languages. Datalog and relational algebra. Logic and recursion.
There is not one particular book that covers the course material entirely. For this reason there will be a set of notes.