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.

Authors

• Heidi E. Dixon Matthew L. Ginsberg
• David K. Hofer Eugene M. Luks

Keywords

No keywords are indexed for this paper.