Go to Main Content

SCT WWW Information System



Detailed Course Information


Fall 2019 Semester
Aug 02, 2021
Transparent Image
Information 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

Must be enrolled in one of the following Levels:     

Undergraduate level CS 2800 Minimum Grade of D- and Undergraduate level CS 3000 Minimum Grade of D-

Return to Previous New Search
Transparent Image
Skip to top of page