Science - Course - Logic and Automated Reasoning

Elementary set theory. Propositional logic. Propositional logic reasoning using resolution. Normal forms, clauses, resolution. First-order/predicate logic introduction. Quantifiers, first order models, validity and satisfiability. First-order reasoning using unrestricted resolution. Normal forms, clauses, Skolemization. Elimination of quantifiers, unification, resolution, simplification techniques. Orderings. Well-founded orderings, lexicographic combinations of orderings, multi-sets, multi-set orderings, reduction orderings, lexicographic path orderings. Refutational completeness of propositional resolution. Herbrand interpretations, soundness, clause orderings, construction of candidate models, reduction of counter-examples, model existence theorem, refutational completeness, compactness of propositional logic. Refutational completeness of first-order resolution. Horn clauses, SLD resolution. Pre-req.: CMPS 445 & CMPS 248