Detailed Course Information |
Spring 2024 Semester
Oct 31, 2024 |
|
 |
||
 | Select the desired Level or Schedule Type to find available classes for the course. |
| CS 4820 - Computer-Aided Reasoning |
|
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.
4.000 Credit hours 4.000 Lecture hours Levels: Undergraduate Schedule Types: Lecture Computer Science Department Course Attributes: NUpath Capstone Experience, Computer&Info Sci Restrictions: Must be enrolled in one of the following Levels: Undergraduate Prerequisites: Undergraduate level CS 2800 Minimum Grade of D- and Undergraduate level CS 3000 Minimum Grade of D- |
| Return to Previous | New Search |
|