COL703 – Logic for Computer Science

Course policy and introduction

• The Lady or the Tiger, by Raymond Smullyan

• To Mock A Mockingbird, also by Raymond Smullyan

Sets, functions, and relations

• Chapters 4 and 8 of Mathematics for Computer Science, by Eric Lehman, F Thomas Leighton, and Albert R Meyer

Orderings and induction

• Introductory notes on Mathematical Induction by Mary Barnes and Sue Gordon

• Section 14 in Naive Set theory by Paul Halmos, PDF found here

Propositional logic

Propositional logic (contd.)

More propositional logic

Here is a link where you can play around with equivalences and normal forms for various expressions. Make sure that you use the English language toggle on the top right if it loads in Dutch. Most of the conversion rules should be easy enough to figure out (they are identities we have covered in class). The only exception is the rule for Equivalence, which is: p ⇔ q iff (p ∧ q) ∨ (¬p ∧ ¬q).

Resolution

The Hilbert system

Completeness for the Hilbert system

Here is a list of proofs you should try to do using the Deduction Theorem. These are fairly fundamental statements and are often useful. Try to do the proofs in order, since some later ones might need you to invoke the ones that came prior.

Here is a link where you can play around with proofs in the Hilbert system. Make sure that you use the English language toggle on the top right if it loads in Dutch. The three axioms are called A, B, and C. A and B are the same as our H1 and H2, but axiom C is taken to be (NOT p IMPLIES not q) IMPLIES (q IMPLIES p).

Propositional logic: Wrap up

This link has an excellent write-up about the Compactness Theorem and the Graph Colouring application.

Murdle is an excellent, fun way to sharpen your logical inference skills. Try to code up today's Murdle in propositional logic! (You need to come up with the right propositions and the right connectives. This will often require some human meta-reasoning using the given clues.)

Z3 Walkthrough

You can play around with other Z3 exercises here. Z3 is a solver that primarily tries to solve the Satisfiability problem, which is known to be hard. However, the problem is so common across subfields that enterprising computer scientists have come up with inventive ways to solve this problem anyway. Recommended reading related to SAT solving includes the DPLL algorithm (which is related to Resolution) and Conflict-Driven Clause Learning (which tries to "learn" a satisfying valuation for the given expression). Come talk to me if you're interested in learning more or working on extensions of any of these!

First-order logic

More first-order logic

Review lecture

FO: Truth and models

FO: Normal forms

Unification

Unification and resolution

FO resolution

This link is an excellent repository of exercises that you can try out to get better both at modelling "real life" statements in FOL, and at performing resolution (to prove the conclusion from the axioms).

FO Resolution is often used in automated theorem proving. Here is a nice little implementation in Python. Caveat: Theorem proving using resolution is not complete (why not?), since the rule does not yield a complete proof system for FOL (unlike the PL resolution rule), so you might not be able to prove everything you might want to.

FO completeness

FO completeness

Natural deduction for FOL

More natural deduction

Here is a list of proofs you should try to do using the natural deduction proof system.

This is a paper that we recently wrote that was accepted at IEEE CSF 2024 showing the (rather nice) NP-completeness for a security system built on top of a positive existential fragment of intuitonistic FOL.
Here is a (perhaps more accessible) older paper that shows algorithms and complexity bounds for various fragments of intuitionistic propositional logic, and essentially points to disjunction as a culprit for the increased complexity of proof search.
Come talk to me if you're interested in doing some work along these lines!

First-order theories

More about First-order theories

Incompleteness

This book by Peter Smith provides a lovely, concise introduction to Gödel's Incompleteness theorem. The technique is slightly different from the ones in the notes, but it is a thoroughly approachable text.

This very interesting piece by Torkel Franzén presents a view of the overall context into which the Incompleteness theorem fits. This cute article by Karl Sigmund describes setting up an exhibition in Vienna in 2006 on the centenary of Gödel's birth, with a very entertaining tapestry of the history of his life and times. These pieces appeared in the Notices of the AMS, volume 53, number 4 (A tribute to Kurt Gödel).

Hoare logic

The original CACM article by Tony Hoare, which introduced Hoare logic can be found here.

This is a fairly comprehensive survey about Hoare logic, written in 2019 to mark fifty years of the CACM article by Tony Hoare which originally introduced the logic. It gives some history of what had come before, and how Hoare logic applies to various kinds of systems one might want to develop and verify.

There are a couple of pedagogical tools one can use to learn Hoare logic better. One is the HAHA system, developed at the University of Warsaw. Another, which helpfully has an in-browser version, is the KeY-Hoare tool, developed by folks from Karlsruhe Institute of Technology, Chalmers University of Technology, and TU Darmstadt.

Hoare logic, more logic