CS180H Proposal
Resolution Proving Experiments
Cathy Block (digitalschoolroom@hotmail.com)
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.
|