Implementing a Generalized Version of Resolution

We have recently proposed augmenting clauses in a Boolean database with groups of permutations, the augmented clauses then standing for the set of all clauses constructed by acting on the original clause with a permutation in the group. This approach has many attractive theoretical properties, including representational generality and reductions from exponential to polynomial proof length in a variety of settings. In this paper, we discuss the issues that arise in implementing a group-based generalization of resolution, and give preliminary results describing this procedure's effectiveness.

• Type: Conference
• Year: 2004
• Where: AAAI
• Authors: Heidi E. Dixon, Matthew L. Ginsberg, David K. Hofer, Eugene M. Luks, Andrew J. Parkes
• Keywords: AAAI 2004, Attractive Theoretical Properties, Augmented Clauses, Intelligent Agents, Polynomial Proof Length