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, includ-ing representational generality and reductions from exponen-tial 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 prelimi-nary results describing this procedure’s effectiveness.