#Logic Syntax and Semantics of Propositional Logic Analytic Tableaux Hilbert Style Proof System Natural Deduction Normalisation in Natural Deduction Proofs Terms, substitution, unification, resolution ROBDDs