CS 4860

CS 4860

Course information provided by the 2025-2026 Catalog.

Topics chosen from propositional logic, first-order logic, and higher-order logic, both classical and intuitionistic versions, including completeness, incompleteness, and compactness results. Natural deduction and tableaux style logics and connection to the lambda calculus and programming languages and logics, and program verification. Other topics chosen from equational logic, Herbrand universes and unification, rewrite rules and Knuth-Bendix method, and the congruence-closure algorithm and lambda-calculus reduction strategies. Modal logics, intuitionistic logic, computational logics and programming languages (e.g., LISP, ML, or Nuprl). Students will be expected to be comfortable writing proofs. More experience with proofs may be gained by first taking a 3000-level MATH course.


Prerequisites MATH 2210, MATH 2230, MATH 2310, MATH 2940, or equivalent.

Forbidden Overlaps CS 4860, MATH 4810, MATH 4860, PHIL 4310

Distribution Requirements (SMR-AS)

Last 4 Terms Offered 2023FA, 2021FA, 2020FA, 2019FA

View Enrollment Information

Syllabi: none
  •   Regular Academic Session.  Combined with: MATH 4860

  • 3 Credits Stdnt Opt

  •  8822 CS 4860   LEC 001

    • TR
    • Jan 20 - May 5, 2026
    • Nerode, A

  • Instruction Mode: In Person