ECE 208: Discrete Mathematics and Logic 2

Sources and References

Equivalent UW courses — CS 245 (Logic and Computation), CS 360 (Intro to the Theory of Computing), MATH 239 (Intro to Combinatorics, loosely related via discrete-math overlap only)

Primary textbook — M. Ben-Ari, Mathematical Logic for Computer Science, 3rd edition, Springer-Verlag, London, 2012. ISBN 978-1-4471-4128-0.

Supplementary references — Huth and Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, 2nd ed., Cambridge, 2004; Bradley and Manna, The Calculus of Computation, Springer, 2007; Biere, Heule, van Maaren, and Walsh (eds.), Handbook of Satisfiability, IOS Press, 2009.

Equivalent UW Courses

ECE 208 is almost entirely a mathematical-logic course and aligns most closely with CS 245, which covers propositional and first-order logic, natural deduction, soundness and completeness, and applications to program verification. CS 360 is the nearest theory-of-computation companion and overlaps on SAT, decidability, and the undecidability arguments of Church and Turing. Despite the “Discrete Mathematics” label, the course has almost no overlap with MATH 239’s combinatorics content (generating functions, graph theory, bijections); MATH 239 only appears as an equivalent insofar as both belong to the discrete-math umbrella. CS 245 is the single best CS-side analogue.

What This Course Adds Beyond the Equivalents

ECE 208 puts more emphasis on deductive systems designed for automation than CS 245 typically does. Binary decision diagrams, propositional resolution, and the architecture of modern SAT solvers (DPLL, conflict-driven clause learning) are first-class topics, whereas CS 245 tends to treat them briefly or omit them. The course also connects logic directly to engineering applications: hardware and software verification, model checking, and temporal logics used in later ECE courses (327, 451, 453, 457). It omits the heavy program-semantics and Hoare-logic treatment that CS 245 emphasizes for software correctness, and it does not develop computability theory to the depth CS 360 does.

Topic Summary

Propositional Logic: Syntax and Semantics

Formulas over a fixed set of atomic propositions built with the usual connectives. An interpretation assigns each atom a truth value in \(\{T, F\}\), and a formula is a tautology if it evaluates to \(T\) under every interpretation. Key meta-properties are satisfiability, validity, and logical consequence \(\Gamma \models \varphi\).

Deductive Systems for Propositional Logic

Hilbert-style systems with a small set of axiom schemas and modus ponens as the sole rule. Proofs are sequences of formulas where each entry is either an axiom, a hypothesis, or derived by a rule. Soundness guarantees that provability implies semantic entailment; completeness is the converse.

Binary Decision Diagrams

Reduced ordered BDDs provide a canonical, compact representation of Boolean functions. Building a BDD by Shannon expansion on a fixed variable order, then applying reduction rules (merge isomorphic subgraphs, eliminate nodes whose children are equal) yields a unique normal form that makes equivalence checking trivial.

Propositional Resolution

A single-rule refutation procedure on clauses in conjunctive normal form. Given clauses containing \(\ell\) and \(\neg \ell\), the resolvent is their union minus the complementary pair. A CNF formula is unsatisfiable iff the empty clause can be resolved from it.

SAT Solvers

DPLL as the backbone: unit propagation, pure-literal elimination, and branching. Modern CDCL solvers add conflict analysis, learned clauses, non-chronological backtracking, and activity-based variable heuristics. Encoding combinatorial and verification problems as SAT instances is treated as a practical skill.

First-Order Logic: Syntax and Semantics

Terms, predicates, functions, and quantifiers \(\forall\) and \(\exists\). A first-order structure consists of a non-empty domain together with interpretations of the symbols; truth is defined inductively, with variable assignments handling free variables. Quantifier scope and substitution (avoiding variable capture) are made precise.

Deductive Systems for First-Order Logic

Hilbert-style axioms extended with quantifier rules (universal generalization, instantiation). The course discusses soundness and completeness at a high level and contrasts the proof-theoretic view with the model-theoretic view. Gödel’s incompleteness and the undecidability of first-order validity (Church-Turing) are stated as fundamental limits, motivating both model checking and interactive theorem proving.