Propositional and predicate logics: syntax and semantics, validity and inference, etc. Deductive tableaux notation and its rules: resolution, equality, equivalence, and rewriting. Axiomatic theories and theories with induction. Verification of implementation and specification using deductive tableaux.