Go to Main Content

SCT WWW Information System

 

HELP | EXIT

Detailed Course Information

 

Fall 2024 Semester
Nov 21, 2024
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

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
Transparent Image
Skip to top of page
Release: 8.7.2.4