CS 4860: Applied Logic (also MATH 486)Cross-Listing: MATH 4860 (CS is parent) Propositional and predicate logic, compactness and completeness by tableaux, natural deduction, and resolution. Equational logic. Herbrand Universes and unification. Rewrite rules and equational logic, Knuth-Bendix method and the congruence-closure algorithm and lambda calculus reduction strategies. Topics in Prolog, LISP, ML, or Nuprl. Applications to expert systems and program verification. Offered: Spring only Prerequisites: MATH 2220 or 2940, CS 2800 or equivalent (such as MATH 3320, 4320, 4340, 4810), and some additional course in math or theoretical computer science. Grade options: Letter or S/U Credit hours: 4 Recent offerings:
|