Abstract
We show that T(F)/ =E can be completely axiomatized when =E is a quasi-free theory. Quasi-free theories are a wider class of theories than permutative theories of [Mal71] for which Mal'cev gave decision results. As an example of application, we show that the first order theory of T(F)/ =E is decidable when E is a set of ground equations. Besides, we prove that the ∑1-fragment of the theory of T(F)/ =E is decidable when E is acompact set of axioms. In particular, the existential fragment of the theory of associative-commutative function symbols is decidable.
This work was partly supported by the Greco de Programmation du CNRS and partly by the Esprit Basic Research Action COMPASS
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
H. J. Bürckert, A. Herold, and Manfred Schmidt-Schauß. On equational theories, unification and decidability. In Proc. Rewriting Techniques and Applications 87, Bordeaux, LNCS 256, pages 204–215. Springer-Verlag, May 1987. Also in C. Kirchner ed. Unification, Academic Press, 1990.
H. J. Bürckert. Solving disequations in equational theories. In Proc. 9th Conf. on Automated Deduction, Argonne, LNCS 310, Springer-Verlag, May 1988.
Hubert Comon and Pierre Lescanne. Equational problems and disunification. J. Symbolic Computation, 7:371–425, 1989.
Hubert Comon. Disunification: a survey. In Jean-Louis Lassez and Gordon Plötkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1990. to appear.
Hubert Comon. Equational formulas in order-sorted algebras. In Proc. ICALP, Warwick. Springer-Verlag, July 1990.
Hubert Comon. Solving inequations in term algebras. In Proc. 5th IEEE Symposium on Logic in Computer Science, Philadelphia, June 1990.
H. Comon. Complete axiomatizations of some quotient term algebras. Research report, LRI and CNRS, Univ. Paris-Sud, 1991.
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–309. North-Holland, 1990.
M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. Research Report IT 182, Laboratoire d'Informatique Fondamentale de Lille, Université des Sciences et Techniques de Lille Flandres Artois, France, March 1990. Also in Proc. 5th IEEE LICS, Philadelphia.
Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In Jean-Louis Lassez and Gordon Plötkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT-Press, 1990. to appear.
Jean-Pierre Jouannaud. Syntactic theories. In B. Rovan, editor, Proc. MFCS 90, Banskà Bystrica, LNCS 452, 1990.
Claude Kirchner. Méthodes et Outils de Conception Systématique d'Algorithmes d'Unification dans les Théories equationnelles. Thèse d'Etat, Univ. Nancy, France, 1985.
Claude Kirchner and F. Klay. Syntactic theories and unification. In Proc. 5th IEEE Symp. Logic in Computer Science, Philadelphia, June 1990.
J.-L. Lassez, M. J. Maher, and K. G. Marriot. Unification revisited. In Proc. Workshop on Found. of Logic and Functional Programming, Trento, LNCS 306. Springer-Verlag, December 1986.
M. J. Maher. Complete axiomatizations of the algebras of finite, rational and infinite trees. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, pages 348–357, July 1988.
A. I. Mal'cev. Axiomatizable classes of locally free algebras of various types. In The Metamathematics of Algebraic Systems. Collected Papers. 1936–1967, pages 262–289. North-Holland, 1971.
Tobias Nipkow. Proof transformations for equational theories. In Proc. 5th IEEE Symp. Logic in Computer Science, Philadelphia, June 1990.
G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27:356–364, 1980.
J. R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967.
R. Treinen. A new method for undecidability proofs of first order theories. Tech. Report A-09/90, Universität des Saarladandes, Saarbrücken, May 1990.
Sauro Tulipani. Decidability of the existential theory of infinite terms with subterm relation. Unpublished Draft, October 1990.
K. N. Venkataraman. Decidability of the purely existential fragment of the theory of term algebras. Journal of the ACM, 34(2):492–510, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Comon, H. (1991). Complete axiomatizations of some quotient term algebras. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds) Automata, Languages and Programming. ICALP 1991. Lecture Notes in Computer Science, vol 510. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54233-7_156
Download citation
DOI: https://doi.org/10.1007/3-540-54233-7_156
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54233-9
Online ISBN: 978-3-540-47516-3
eBook Packages: Springer Book Archive