Advisor: Dr. Chris Pollett

Description:

This independent study project (CS 180H) will focus on two methods of proving validity. The first is the Davis, Logemann and Loveland version of the Davis-Putnam algorithm (DPLL algorithm) as described by Russell and Novig (2003, p. 221 - 222). The second is the Groebner Basis algorithm, as described by Clegg, Edmonds and Impagliazzo (1996, May p. 174 - 183). Both algorithms will be implemented and compared. The implementations will be in Java with an Applet interface. Input will be propositional sentences in disjunctive normal form. A Tau tautology generator may also be created to compare the performance of the two algorithms. Deliverables will consist of a Java Applet implementation of both algorithms with standard documentation, as well as any comparison data.

References:

Clegg, M., Edmonds, J., & Impagliazzo, R. (1996, May). Using the Groebner basis algorithm to find proofs of unsatisfiability. Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, 174-183, Philadelphia, Pennsylvania.

Russell, S. & Novig, P. (2003). Artificial Intelligence: A Modern Approach (2nd ed.). Upper Saddle River, NJ: Pearson Education Inc.