Implementing a Generalized Version of Resolution

Abstract

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.

Cite

Text

Dixon et al. "Implementing a Generalized Version of Resolution." AAAI Conference on Artificial Intelligence, 2004.

Markdown

[Dixon et al. "Implementing a Generalized Version of Resolution." AAAI Conference on Artificial Intelligence, 2004.](https://mlanthology.org/aaai/2004/dixon2004aaai-implementing/)

BibTeX

@inproceedings{dixon2004aaai-implementing,
  title     = {{Implementing a Generalized Version of Resolution}},
  author    = {Dixon, Heidi E. and Ginsberg, Matthew L. and Hofer, David K. and Luks, Eugene M. and Parkes, Andrew J.},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2004},
  pages     = {55-60},
  url       = {https://mlanthology.org/aaai/2004/dixon2004aaai-implementing/}
}