This page links to the interactive notes and exercises for Logic part of CS208 Logic & Algorithms, part of the Undergraduate BSc (Hons) /MEng Computer Science and BSc (Hons) Software Engineering degrees at the University of Strathclyde.
Please send any comments, queries, or corrections to Robert Atkey (Web page). The source code for these pages in available on Github.
Introduction
In the first semester of CS208, we will study Symbolic Logic. Symbolic Logic is a fundamental set of techniques for describing situations, reasoning, data, and processes. It is useful in computing for describing, building, and checking systems, and for solving complicated problems involving many interacting constraints. 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 (Strathclyde students only) 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 0: Propositional Logic
Part 0 of this course is a (re)introduction to the basic concepts of Propositional Logic.
Syntax: what are the valid sequences of symbols that we can write down? Which ones are logical formulas?
Semantics: what do those symbols mean? What do formulas made from the symbols mean?
Truth Tables, Satisfiability, and Validity: An effective way to compute the meaning of a logical formula, and two kinds of statements we can make about a formula.
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.
How to handle bigger problems with domains and parameters.
SAT solvers, the underlying technology.
Resource allocation problems, which are a kind of graph colouring problem.
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. We also look at a use of circuits to solve problems that are hard to solve directly.
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 linked below. 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? What does mathematics mean?
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.
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?
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 and false anymore, but about relationships between individuals.
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.
Specifying Properties of Programs. We can use predicate logic to make precise some statements we can make about programs and how they execute.
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?