| The object of automated reasoning is to write computer programs that can assist in the solving of problems and the answer of questions that require reasoning. Most of the work in this field in the last 30 years has used Robinson's resolution method (1965). The main part of this course deals with the clause tree data structure/technique developed by the instructors since 1993. The relationship between clause trees and other techniques are also covered, including: Loveland's chain technique (1969), Bibel's connection method (1980), the tableaux method, the connection tableau calculi of Letz, Mayr and Goller (1994), and the clause graph resolution (connection graphs) of Kowalski and Eisinger. Prerequisite: An undergraduate course in algorithms (e.g. CS 3933). |
