This page links to the interactive notes and exercises for Logic part of CS208 Logic & Algorithms, part of the Undergraduate Computer Science degree at the University of Strathclyde.
Please send any comments and queries to Robert Atkey (Web page). The source code for these pages in available on Github.
Introduction
In the first half of the course, we will study Symbolic Logic. Symbolic Logic is a fundamental set of the techniques for describing data and processes. It is useful in computing for describing, building and checking systems. We will look at how to define logic (syntax and semantics), algorithms for computing with logic, and systems for deriving proofs in formal logic. We will also keep in mind the practical uses of logic in Computer Science.
This course follows on from CS103 and CS106 in first year.
Please see the MyPlace page for information on Lectures, Tutorials, and Assessment.
Learning Outcomes
By the end of semester 1 of the module you should be able to:
Understand formulas of Propositional and Predicate Logic
Use Propositional and Predicate Logic to model problems and their solutions
Understand how a SAT solver works and how it can be used to solve problems
Construct proofs in Propositional and Predicate Logic
Understand the basic metatheory of Propositional and Predicate Logic
Part 1: Logical Modelling
In Part 1, we use logical modelling to describe and solve problems.
Introduction to Logical Modelling and the Logical Modelling tool.
The Wizard's Pets, introducing some common kinds of constraints through a toy example.
Patterns for writing logical constraints.
A fruity exercise for you to do.
SAT solvers, the underlying technology.
How to handle bigger problems with domains and parameters.
Resource allocation problems, which are a kind of graph colouring problem. (under construction)
Converting to CNF. SAT solvers take their input in CNF. Some problems are naturally in CNF (like the Packages or Resource Allocation problems above), but sometimes we need to convert any formula to one in CNF.
Circuits, Gates and Formulas, where we look at encoding logic gates as clauses, using the Tseytin transformaion. We can then get the solver to answer questions about circuits.
Coursework: Coursework 1 is here.
Part 2: Deductive proof and Predicate Logic
In Part 2, we strive for truth through proof. We will be using an interactive proof editor to construct natural deduction proofs. Exercises with fixed things to prove are embedded in each of the pages. You can also enter your own things to prove on this page.
Introduction to Deductive Proof, which describes the general idea of proof systems, and introduces a small example of a proof system inspired by biology.
Natural Deduction and the rules for And. Natural Deduction is a style of proof system that places a particular emphasis on how assumptions are used, and on how the rules for each connective come in introduction and elimination pairs.
Proof rules for Implication. Implication allows us to make conditional statements that we prove by temporarily making assumptions.
Proof rules for Or and Not, which complete the rules for the connectives of Propositional Logic.
Soundness and Completeness, and some Philosophy. The system so far is sound, but is it complete? Should it be complete?
Introducing Predicate Logic as an expressive language for making statements in a formalised way. By selecting our vocabulary carefully, we can use Predicate Logic as a modelling tool to describe many situations.
Scoping and Substitution. Before we look at proof for Predicate Logic, we need to upgrade our Natural Deduction system to handle assumptions about entities as well as propositions. This brings us to the matters of scope and substitution.
Proof rules for Predicate Logic. Natural deduction rules for “for all” and “exists” allow us to construct proofs of Predicate Logic formulas.
Predicate Logic Semantics. A break from proof for a bit to consider what Predicate Logic formulas are talking about. It is not just about true/false anymore, but about relationships between individuals.
Equality. How do we prove that one thing is equal to another thing? And what can we prove if we know that one thing is equal to another thing?
Arithmetic and Induction. Induction allows us to prove facts about infinitely many individuals, as long as those individuals are built up in a “well founded” way. We look specifically at induction on natural numbers, which will allow us to prove facts in the theory of arithmetic as described by Peano's axioms.
Undecidability of the Halting Problem. One of the foundational results of Computer Science is that there is no program which can reliably tell if another program will halt on a given input. This page goes through a formal proof of this fact.
Metatheory and Gödel's Incompleteness Theorem. If we as humans can construct proofs, then could we get a computer to do it? What are the limits of what we can prove?