Proceedings

On the Complexity of Extending Ground Resolution with Symmetry Rules

Thierry Boy de la Tour, Stéphane Demri

Download BibTeX Cite

Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 289-296.

Abstract

One important issue of automated theorem proving is the complexity of the inference rules used in theorem provers. If Krishnamurty's general symmetry rule is to be used, then one should provide some way of computing non trivial symmetries. We show that this problem is NP-complete . But this general rule can be simplified by restricting it to what we callSsymmetries, yielding the well-known symmetry rule. We show that computing S-symmetries is in the same complexity class as the graph isomorphism problem, which appears to be neither polynomial nor NP-complete . However it is sufficient to compute the set of all S-symmetries at the beginning of the proof search, and since it is a permutation group, there exist some efficient techniques from computational group theory to represent this set . We also show how these techniques can be used for applying the S-symmetry rule in polynomial time.

Thierry Boy de la Tour, and Stephane Demri. 1995. On the Complexity of Extending Ground Resolution with Symmetry Rules. In Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI-95. IJCAI, 289–296. https://ijcai.org/proceedings/1995/38
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards