Computer Science
CS 4820: Computer-Aided Reasoning
Lecture - 4 credits
ND
EI
IC
FQ
SI
AD
DD
ER
WF
WD
WI
EX
CE
- 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.
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. Show more.