Queen's School of Computing

CISC 204/3.0 Logic for Computing Science

Original Author: Bob Tennent
Last Revised: September 26, 2006

Calendar Description
Elements of mathematical logic with computing applications. Formal proof systems for propositional and predicate logic. Interpretations, validity, and satisfiability. Introduction to soundness, completeness and decidability.
Learning Hours: 120 (36L;84P)

Prerequisite: Level 2 or above and CISC 121/3.0 and (CISC 102/3.0 or CISC 203/3.0 or MATH 110/6.0)

This course is a direct prerequisite for

  • CISC-332/3.0 (Database Systems)
  • CISC-365/3.0 (Algorithms),

and a co-requisite for

  • CISC-223/3.0 (Software Specifications)
  • CISC-260/3.0 (Programming Paradigms)

This course is required in all Computing programs.

Review of elementary logic (2 weeks)
  • propositions
  • connectives
  • truth tables
  • converse and contrapositive
  • tautologies and satisfiability
  • logical implications and equivalences, de Morgan's laws
  • normal forms
  • quantifiers and predicates
  • free and bound variables, scope
  • logical equivalences for quantifiers
  • conventional (informal) proof methods by example: proof by cases, proof by contradiction, etc.
  • terminology: hypothesis, conclusion, conjecture, corollary, lemma, etc.
  • mathematical induction (on the natural numbers)
Propositional logic (4 weeks)
  • propositional logic as a formal language
  • structural induction (induction on syntax)
  • semantics of propositional logic
  • satisfiability, semantic entailment and semantic equivalence
  • the natural-deduction system for propositional logic: conjunction and implication, negation and disjunction
  • proof of soundness of the system of propositional logic (outline)
  • completeness of the system of propositional logic (definition and statement of result only)
  • decidability of the system of propositional logic (definition and statement of result only)
Predicate logic (4 weeks)
  • variables, quantifiers, terms and formulas
  • substitution, variable capture, change of bound variable
  • natural deduction rules for predicate logic: universal quantifier, existential quantifier, side conditions
  • models, environments (assignments of values to variables)
  • soundness, completeness and undecidability of predicate logic (statements of results only)

Use of a proof checking or theorem proving tool such as Jape, Isabelle, PVS, or Hyperproof is strongly recommended.

Possible Textbooks
  • Logic and Structure van Dalen (Springer, 1994)
  • Introductory Logic and Sets for Computer Scientists, Nissanke (Addison-Wesley, 1999)
  • Logic in Computer Science, Modelling and Reasoning About Systems, Huth and Ryan (2nd edition, CUP, 2004)
  • Mathematical Logic for Computer Science, Ben-Ari (Springer, 2001)
  • Logic and its Applications, Burke and Foxley (Prentice-Hall Int., 1996)
  • Reasoned Programming (Part II), Broda et al. (Prentice-Hall Int., 1994)
  • The Essence of Logic, Kelly (Prentice-Hall, 1997)
  • Logic for Computer Science, Reeves and Clarke (Addison-Wesley, 1990) (out of print, but still available)