×

Decidability and complexity of simultaneous rigid E-unification with one variable and related results. (English) Zbl 0944.68103

Summary: We show that simultaneous rigid E-unification, or SREU for short, is decidable and in fact EXPTIME-complete in the case of one variable. This result implies that the \(\forall^{*}\exists \forall^{*}\) fragment of intuitionistic logic with equality is decidable. Together with a previous result regarding the undecidability of the \(\exists \exists\)-fragment, we obtain a complete classification of decidability of the prenex fragment of intuitionistic logic with equality, in terms of the quantifier prefix. It is also proved that SREU with one variable and a constant bound on the number of rigid equations is P-complete. Moreover, we consider a case of SREU where one allows several variables, but each rigid equation either contains one variable, or has a ground left-hand side and an equality between two variables as a right-hand side. We show that SREU is decidable also in this restricted case.

MSC:

68Q45 Formal languages and automata
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Andrews, P. B., Theorem proving via general matings, J. Assoc. Comput. Mach., 28, 2, 193-214 (1981) · Zbl 0456.68119
[2] Bibel, W., Deduction. Automated Logic (1993), Academic Press: Academic Press New York · Zbl 0677.68094
[3] Brainerd, W. S., Tree generating regular systems, Inform. Control, 14, 217-231 (1969) · Zbl 0169.31601
[4] Chang, C. C.; Keisler, H. J., Model Theory (1990), North-Holland: North-Holland Amsterdam · Zbl 0697.03022
[5] Coquidé, J. L.; Dauchet, M.; Gilleron, R.; Vágvölgyi, S., Bottom-up tree pushdown automata: classification and connection with rewrite systems, Theoret. Comput. Sci., 127, 69-98 (1994) · Zbl 0805.68083
[6] Courcelle, B., On recognizable sets and tree automata, (Nivat, M.; Ait-Kaci, H., Resolution of Equations in Algebraic Structures (1989), Academic Press: Academic Press New York)
[7] Dauchet, M., Rewriting and tree automata, (Comon, H.; Jouannaud, J. P., Term Rewriting (French Spring School of Theoretical Computer Science), Lecture Notes in Computer Science, vol. 909 (1993), Springer: Springer Berlin)
[8] M. Dauchet, T. Heuillard, P. Lescanne, S. Tison, Decidability of the confluence of ground term rewriting systems, Proc. IEEE Conf. on Logic in Computer Science (LICS), IEEE Computer Society Press, Silver Spring, MD, 1987, pp. 353-360.; M. Dauchet, T. Heuillard, P. Lescanne, S. Tison, Decidability of the confluence of ground term rewriting systems, Proc. IEEE Conf. on Logic in Computer Science (LICS), IEEE Computer Society Press, Silver Spring, MD, 1987, pp. 353-360. · Zbl 0705.68067
[9] M. Dauchet, S. Tison, Tree automata and decidability in ground term rewriting systems, Proc. FCT’85, Lecture Notes in Computer Science, vol. 199, 1985, pp. 80-84.; M. Dauchet, S. Tison, Tree automata and decidability in ground term rewriting systems, Proc. FCT’85, Lecture Notes in Computer Science, vol. 199, 1985, pp. 80-84. · Zbl 0579.68023
[10] M. Dauchet, S. Tison, The theory of ground rewrite systems is decidable, Proc. IEEE Conf. on Logic in Computer Science (LICS), IEEE Computer Society Press, Silver Spring, MD, 1990, pp. 242-248.; M. Dauchet, S. Tison, The theory of ground rewrite systems is decidable, Proc. IEEE Conf. on Logic in Computer Science (LICS), IEEE Computer Society Press, Silver Spring, MD, 1990, pp. 242-248.
[11] De Kogel, E., Rigid \(E\)-unification simplified, (Baumgartner, P.; Hähnle, R.; Posegga, J., Theorem Proving with Analytic Tableaux and Related Methods, Lecture Notes in Artificial Intelligence, vol. 918 (1995), Schloß Rheinfels: Schloß Rheinfels St. Goar, Germany)
[12] A. Degtyarev, Yu. Gurevich, A. Voronkov, Herbrand’s theorem and equational reasoning: problems and solutions, Bulletin of the European Association for Theoretical Computer Science, vol. 60, The Logic in Computer Science column, October 1996.; A. Degtyarev, Yu. Gurevich, A. Voronkov, Herbrand’s theorem and equational reasoning: problems and solutions, Bulletin of the European Association for Theoretical Computer Science, vol. 60, The Logic in Computer Science column, October 1996. · Zbl 0866.68102
[13] A. Degtyarev, Yu. Matiyasevich, A. Voronkov, Simultaneous rigid \(E\); A. Degtyarev, Yu. Matiyasevich, A. Voronkov, Simultaneous rigid \(E\)
[14] A. Degtyarev, Yu. Matiyasevich, A. Voronkov, Simultaneous rigid \(E\); A. Degtyarev, Yu. Matiyasevich, A. Voronkov, Simultaneous rigid \(E\)
[15] A. Degtyarev, A. Voronkov, Simultaneous rigid \(E\); A. Degtyarev, A. Voronkov, Simultaneous rigid \(E\) · Zbl 0872.68173
[16] A. Degtyarev, A. Voronkov, Decidability problems for the prenex fragment of intuitionistic logic, 11th Ann. IEEE Symp. on Logic in Computer Science (LICS’96), New Brunswick, NJ, July, IEEE Computer Society Press, Silver Spring, MD, 1996, pp. 503-512.; A. Degtyarev, A. Voronkov, Decidability problems for the prenex fragment of intuitionistic logic, 11th Ann. IEEE Symp. on Logic in Computer Science (LICS’96), New Brunswick, NJ, July, IEEE Computer Society Press, Silver Spring, MD, 1996, pp. 503-512.
[17] A. Degtyarev, A. Voronkov, Simultaneous rigid \(E\); A. Degtyarev, A. Voronkov, Simultaneous rigid \(E\)
[18] Degtyarev, A.; Voronkov, A., The undecidability of simultaneous rigid \(E\)-unification, Theoret. Comput. Sci., 166, 1-2, 291-300 (1996) · Zbl 0872.68173
[19] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (Van Leeuwen, J., Handbook of Theoretical Computer Science, vol. B: Formal Methods and Semantics, ch. 6 (1990), North-Holland: North-Holland Amsterdam), 243-309 · Zbl 0900.68283
[20] Doner, J., Tree acceptors and some of their applications, J. Comput. System Sci., 4, 406-451 (1970) · Zbl 0212.02901
[21] Fitting, M., First-order modal tableaux, J. Automat. Reason., 4, 191-213 (1988) · Zbl 0648.03004
[22] T. Frühwirth, E. Shapiro, M. Vardi, E. Yardeni, Logic programs as types of logic programs, Proc. 6th Symp. on Logics in Computer Science (LICS), 1991, pp. 300-309.; T. Frühwirth, E. Shapiro, M. Vardi, E. Yardeni, Logic programs as types of logic programs, Proc. 6th Symp. on Logics in Computer Science (LICS), 1991, pp. 300-309.
[23] Gallier, J.; Narendran, P.; Plaisted, D.; Snyder, W., Rigid \(E\)-unification: NP-completeness and applications to equational matings, Inform. Comput., 87, 1/2, 129-195 (1990) · Zbl 0709.68080
[24] J.H. Gallier, P. Narendran, D. Plaisted, W. Snyder, Rigid \(E\); J.H. Gallier, P. Narendran, D. Plaisted, W. Snyder, Rigid \(E\)
[25] J.H. Gallier, S. Raatz, W. Snyder, Theorem proving using rigid \(E\); J.H. Gallier, S. Raatz, W. Snyder, Theorem proving using rigid \(E\) · Zbl 0799.68171
[26] Gécseg, F.; Steinby, M., Tree Automata (1984), Akadémiai Kiodó: Akadémiai Kiodó Budapest · Zbl 0396.68041
[27] J. Goubault, Rigid \(E\); J. Goubault, Rigid \(E\)
[28] Greenlaw, R.; Hoover, H. J.; Ruzzo, W. L., Limits to Parallel Computation: \(P\)-Completeness Theory (1995), Oxford University Press: Oxford University Press Oxford · Zbl 0829.68068
[29] Y. Gurevich, M. Veanes, Some undecidable problems related to the Herbrand theorem, UPMAIL Technical Report 138, Uppsala University, Computing Science Department, March 1997, Inform. Comput. submitted.; Y. Gurevich, M. Veanes, Some undecidable problems related to the Herbrand theorem, UPMAIL Technical Report 138, Uppsala University, Computing Science Department, March 1997, Inform. Comput. submitted.
[30] Gurevich, Y.; Voronkov, A., Monadic simultaneous rigid \(E\)-unification and related problems, (Degano, P.; Corrieri, R.; Marchetti-Spaccamella, A., Automata, Languages and Programming, 24th International Colloquium, ICALP’97, Lecture Notes in Computer Science, vol. 1256 (1997), Springer: Springer Berlin), 154-165 · Zbl 1401.03037
[31] Kozen, D., Complexity of finitely presented algebras, Technical Report TR 76-294 (1976), Cornell University: Cornell University Ithaca, NY
[32] D. Kozen, Complexity of finitely presented algebras, Proc. 9th Ann. Symp. on Theory of Computing, ACM, New York, 1977, pp. 164-177.; D. Kozen, Complexity of finitely presented algebras, Proc. 9th Ann. Symp. on Theory of Computing, ACM, New York, 1977, pp. 164-177.
[33] D. Kozen, Lower bounds for natural proof systems, Proc. 18th IEEE Symp. on Foundations of Computer Science (FOCS), 1977, pp. 254-266.; D. Kozen, Lower bounds for natural proof systems, Proc. 18th IEEE Symp. on Foundations of Computer Science (FOCS), 1977, pp. 254-266.
[34] Kozen, D., Positive first-order logic is NP-complete, IBM J. Res. Dev., 25, 4, 327-332 (1981) · Zbl 0481.03026
[35] Lankford, D. S., Canonical inference, Technical Report (1975), Department of Mathematics, South-Western University: Department of Mathematics, South-Western University Georgetown, Texas
[36] V. Lifschitz, Problem of decidability for some constructive theories of equalities (in Russian), Zapiski Nauchnyh Seminarov LOMI 4 (1967) 78-85. (English Trans. Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, pp. 29-31).; V. Lifschitz, Problem of decidability for some constructive theories of equalities (in Russian), Zapiski Nauchnyh Seminarov LOMI 4 (1967) 78-85. (English Trans. Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, pp. 29-31).
[37] Loveland, D. W., Mechanical theorem proving by model elimination, J. Assoc. Comput. Mach., 15, 236-251 (1968) · Zbl 0162.02804
[38] G.S. Makanin, The problem of solvability of equations in free semigroups, Mat. Sbornik (in Russian) 103(2) (1977) 147-236. (English Trans. Amer. Math. Soc. Trans. 117 (2) (1981)).; G.S. Makanin, The problem of solvability of equations in free semigroups, Mat. Sbornik (in Russian) 103(2) (1977) 147-236. (English Trans. Amer. Math. Soc. Trans. 117 (2) (1981)). · Zbl 0371.20047
[39] Mezei, J.; Wright, J. B., Algebraic automata and context-free sets, Inform. Control, 11, 3-29 (1967) · Zbl 0155.34301
[40] G.E. Mints, Choice of terms in quantifier rules of constructive predicate calculus (in Russian), Zapiski Nauchnyh Seminarov LOMI 4 (1967) 78-85. (English Trans. Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, pp. 43-46).; G.E. Mints, Choice of terms in quantifier rules of constructive predicate calculus (in Russian), Zapiski Nauchnyh Seminarov LOMI 4 (1967) 78-85. (English Trans. Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, pp. 43-46).
[41] Orevkov, V. P., Unsolvability in the constructive predicate calculus of the class of the formulas of the type \(¬¬∀∃\) (in Russian), Soviet Math. Dokl., 163, 3, 581-583 (1965) · Zbl 0173.01004
[42] V.P. Orevkov, Solvable classes of pseudo-prenex formulas (in Russian), Zapiski Nauchnyh Seminarov LOMI 60 (1976) 109-170 (English Trans. J. Soviet Math.); V.P. Orevkov, Solvable classes of pseudo-prenex formulas (in Russian), Zapiski Nauchnyh Seminarov LOMI 60 (1976) 109-170 (English Trans. J. Soviet Math.) · Zbl 0342.02034
[43] D.A. Plaisted, Special cases and substitutes for rigid \(E\); D.A. Plaisted, Special cases and substitutes for rigid \(E\) · Zbl 0938.03020
[44] Seidl, H., Haskell overloading is DEXPTIME-complete, Inform. Process. Lett., 52, 2, 57-60 (1994) · Zbl 0835.68008
[45] Shostak, R., An algorithm for reasoning about equality, Commun. ACM, 21, 583-585 (1978) · Zbl 0378.68044
[46] Snyder, W., Efficient ground completionAn \(O(n log n)\) algorithm for generating reduced sets of ground rewrite rules equivalent to a set of ground equations \(E\), (Goos, G.; Hartmanis, J., Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 355 (1989), Springer: Springer Berlin), 419-433 · Zbl 1503.68156
[47] Statman, R., Lower bounds on Herbrand’s theorem, Proc. Amer. Math. Soc., 75, 1, 104-107 (1979) · Zbl 0411.03048
[48] Thatcher, J. W.; Wright, J. B., Generalized finite automata theory with an application to a decision problem of second-order logic, Math. Systems Theory, 2, 1, 57-81 (1968) · Zbl 0157.02201
[49] W. Thomas, Languages, automata and logic, Technical Report 9607, Institut für Informatik und Praktische Mathematik der Christian-Albrechts-Universität zu Kiel, 1996, in: G. Rozenberg, A. Salomaa (Eds.), A modified version appears as a chapter of the Handbook of Formal Language Theory, Springer, Berlin.; W. Thomas, Languages, automata and logic, Technical Report 9607, Institut für Informatik und Praktische Mathematik der Christian-Albrechts-Universität zu Kiel, 1996, in: G. Rozenberg, A. Salomaa (Eds.), A modified version appears as a chapter of the Handbook of Formal Language Theory, Springer, Berlin.
[50] M. Veanes, On computational complexity of basic decision problems of finite tree automata, UPMAIL Technical Report 133, Uppsala University, Computing Science Department, January 1997.; M. Veanes, On computational complexity of basic decision problems of finite tree automata, UPMAIL Technical Report 133, Uppsala University, Computing Science Department, January 1997.
[51] M. Veanes, The undecidability of simultaneous rigid \(E\); M. Veanes, The undecidability of simultaneous rigid \(E\) · Zbl 0884.03047
[52] M. Veanes, The relation between second-order unification and simultaneous rigid \(E\); M. Veanes, The relation between second-order unification and simultaneous rigid \(E\) · Zbl 0945.03528
[53] A. Voronkov, Proof search in intuitionistic logic based on constraint satisfaction, in: P. Miglioli, U. Moscato, D. Mundici, M. Ornaghi (Eds.), Theorem Proving with Analytic Tableaux and Related Methods. 5th Int. Workshop, TABLEAUX ’96, Lecture Notes in Artificial Intelligence, vol. 1071, Terrasini, Palermo Italy, May 1996, pp. 312-329.; A. Voronkov, Proof search in intuitionistic logic based on constraint satisfaction, in: P. Miglioli, U. Moscato, D. Mundici, M. Ornaghi (Eds.), Theorem Proving with Analytic Tableaux and Related Methods. 5th Int. Workshop, TABLEAUX ’96, Lecture Notes in Artificial Intelligence, vol. 1071, Terrasini, Palermo Italy, May 1996, pp. 312-329. · Zbl 1415.03010
[54] A. Voronkov, Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\); A. Voronkov, Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\) · Zbl 1415.03011
[55] A. Voronkov, Herbrand’s theorem, automated reasoning and semantic tableaux, Proc. Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS’98), IEEE Computer Society Press, 1998, pp. 252-263.; A. Voronkov, Herbrand’s theorem, automated reasoning and semantic tableaux, Proc. Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS’98), IEEE Computer Society Press, 1998, pp. 252-263. · Zbl 0945.03553
[56] A. Voronkov, Simultaneous rigid \(E\); A. Voronkov, Simultaneous rigid \(E\) · Zbl 0937.03020
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.