CS 4820 — Computer-Aided Reasoning
4 semester hoursUndergraduateLectureNUpath CEusually offered: springtypical days: T/FBostonTraditional
Covers fundamental concepts, techniques, and algorithms in computer-aided reasoning, including propositional logic, variants of the DPLL algorithm for satisfiability checking, first-order logic, unification, tableaux, resolution, Horn clauses, congruence closure, rewriting, Knuth-Bendix completion, decision procedures, Satisfiability Modulo Theories, recursion, induction, termination, Presburger arithmetic, quantifier elimination, and interactive theorem proving. Offers students an opportunity to develop and implement a reasoning engine in a sequence of projects over the course of the semester. Also covers how to formalize and reason about computational systems using a modern interactive theorem prover.
Prerequisites
Offering history
| Term | Sections | Enrolled | Capacity | Full | Open seats/section |
|---|---|---|---|---|---|
| Spring 2026 | 1 | 3 | 10 | 30% | 7.0 |
Snapshots from scheduled scrapes — not live seat availability. "Full" can exceed 100% when sections over-enroll.
Meeting times
Share of recent sections by weekday: M 0% · T 100% · W 0% · Th 0% · F 100%
Common patterns: TF (100% of sections) — in patterns, R means Thursday
Professors
Spring
- Pete Manolios (100% of students) · reviews
Percentages are each professor's average share of the season's enrolled students in recent terms.
Links
Official catalog (CS course descriptions) · Student reviews on RateMyHusky · All CS courses · Plan it at numap.app