COM S 486: Applied Logic (also MATH 486)Cross-Listing: MATH 486 (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 222 or 294, COM S 280 or equivalent (such as MATH 332, 432, 434, 481), and some additional course in math or theoretical computer science. Grade options: Letter or S/U Credit hours: 4 Recent offerings:
|
