×

On the complexity of deduction modulo leaf permutative equations. (English) Zbl 1086.03008

Summary: In the context of equational reasoning, J. Avenhaus and D. Plaisted proposed to deal with leaf permutative equations in a uniform, specialized way. The simplicity of these equations and the useless variations that they produce are good incentives to lift theorem proving to so-called stratified terms, in order to perform deduction modulo such equations. This requires specialized algorithms for standard problems involved in automated deduction. To analyze the computational complexity of these problems, we focus on the group-theoretic properties of stratified terms. NP-completeness results are given and (slightly) relieved by restrictions on leaf permutative theories, which allow us the use of techniques from computational group theory.

MSC:

03B35 Mechanization of proofs and logical operations
03D15 Complexity of computation (including implicit computational complexity)
03F20 Complexity of proofs
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Avenhaus, J. and Plaisted, D.: General algorithms for permutations in equational inference, J. Automated Reasoning 26 (April 2001), 223-268. · Zbl 0985.68026 · doi:10.1023/A:1006439522342
[2] Baader, F. and Nipkow, T.: Term Rewriting and All That, Cambridge University Press, 1998. · Zbl 0948.68098
[3] Babai, L.: Automorphism groups, isomorphism, reconstruction, in R. L. Graham, M. Grotschel and L. Lovasz (eds.), Handbook of Combinatorics, Vol. 2, Elsevier and MIT Press, 1995. · Zbl 0846.05042
[4] Babai, L., Erdõs, P. and Selkow, S. M.: Random graph isomorphism, SIAM J. Computing 9(3) (August 1980), 628-635. · Zbl 0454.05038 · doi:10.1137/0209047
[5] Barendregt, H. P., van Eekelen, M. C. J. D., Glauert, J. R. W., Kennaway, J. R., Plasmeijer, M. J. and Sleep M. R.: Term graph rewriting, in J. W. de Bakker, A. J. Nijman and P. C. Treleaven (eds.), PARLE?87, LNCS 259, Vol. 2, Springer-Verlag, June 1987, pp. 141-158. · Zbl 0681.68037
[6] Boy de la Tour, T. and Echenim, M.: On leaf permutative theories and occurrence permutation groups, in I. Dahn and L. Vigneron (eds.), FTP?2003, Electronic Notes in TCS 86, 2003. · Zbl 1261.68097
[7] Boy de la Tour, T. and Echenim, M.: NP-completeness results for deductive problems on stratified terms, in M. Vardi and A. Voronkov (eds.), LPAR, LNAI 2850, 2003, pp. 315-329. · Zbl 1273.68316
[8] Boy de la Tour, T. and Echenim, M.: Overlapping leaf permutative equations, in D. Basin and M. Rusinowitch (eds.), IJCAR?04, LNAI, 2004. · Zbl 1126.68561
[9] Butler, G.: Fundamental Algorithms for Permutation Groups, Lecture Notes in Comput. Sci. 559, Springer-Verlag, 1991. · Zbl 0785.20001
[10] Furst, M., Hopcroft, J. and Luks, E.: Polynomial time algorithms for permutation groups, in Proceedings 21st Annual Symposium on the Foundations of Computer Science, October 1980, pp. 36-41. · Zbl 0462.05059
[11] Garey, M. and Johnson, D. S.: Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, San Francisco, CA, 1979. · Zbl 0411.68039
[12] Hoffmann, C.: Group-Theoretic Algorithms and Graph Isomorphism, Lecture Notes in Comput. Sci. 136, Springer-Verlag, 1981.
[13] Leon, J. S.: Permutation group algorithms based on partitions, I: Theory and algorithms, J. Symbolic Comput. 12(4-5) (1991), 533-583. · Zbl 0807.20001 · doi:10.1016/S0747-7171(08)80103-4
[14] Schöning, U. and Pruim, R.: Gems of Theoretical Computer Science, Springer-Verlag, 1998. · Zbl 0911.68002
[15] Stickel, M. E.: A unification algorithm for associative-commutative functions, J. ACM 28(2) (April 1981), 423-434. · Zbl 0462.68075 · doi:10.1145/322261.322262
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.