Minimal and complete word unification

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Minimal and complete word unification

Full text

Pdf (2.76 MB)

Source

Journal of the ACM (JACM) archive
Volume 37 , Issue 1 (January 1990) table of contents

Pages: 47 - 85

Year of Publication: 1990

ISSN:0004-5411

Author

Joxan Jaffar

IBM Thomas J. Watson Research Center, Yorktown Heights, NY

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 25, Citation Count: 11

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/78935.78938 What is a DOI?

ABSTRACT

The fundamental satisfiability problem for word equations has been solved recently by Makanin. However, this algorithm is purely a decision algorithm. The main result of this paper solves the complementary problem of generating the set of all solutions. Specifically, the algorithm in this paper generates, given a word equation, a minimal and complete set of unifiers. It stops if this set is finite.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	ABDULRAB, H. Resolution D'Equations sur les mots: Etude et Implementation Lisp de L'Algorithme de Makanin. These doctorat es sciences, Universit6 de Rouen, Rouen, France, Mar. 1987.
	2	BENNETT, J. H. CRT-aided semi-automated mathematics. AFCRL 67-0167. Applied Logic Corporation, Princeton, N.J., 1967.
	3	BULITKO, V.K. Equations and inequalities in a free group and a free semigroup. Tul. Gos. Ped. Inst. Ucen. Zap. Mat. Kafedr Vyp 2, Geometr. i Algebra (1970), 242-252 (in Russian).
	4	COOPER, D. C. Theorem-proving in arithmetic without multiplication. Mach. Int. 7 (1972), 91-99.
	5	HMELEVSKII, JU. I. Equations in free semigroups. Trudy Mat. Inst. Steklov 107 (1971) (English translation; Proc. Steklov Inst. of Mathematics 107 ( 197 l, 1977)), 269 pages.
	6	MAKANIN, G.S. The problem of solvability of equations in a free semigroup. Math. USSR Sbornik 32, 2 (1977), 129-198 (In AMS, (1979)).
	7	Arthur J. Nevins, A Human Oriented Logic for Automatic Theorem-Proving, Journal of the ACM (JACM), v.21 n.4, p.606-621, Oct. 1974 [doi>10.1145/321850.321858]
	8	PECUCHET, J.-P. Equations avec Constantes et Algorithme de Makanin. These 3e Cycle, Universit6 de Rouen, Rouen, France, Dec. 198 I.
	9	PLOTKIN, G.D. Building in equational theories. Mach. Int. 7 (1972), 73-90.
	10	SIEKMANN, J. String unification. Memo CSM-7, Essex Univ., Essex, England, 1975.
	11	Jörg H. Siekmann , Peter Szabó, Universal Unification and a Classification of Equational Theories, Proceedings of the 6th Conference on Automated Deduction, p.369-389, June 07-09, 1982

CITED BY 11

	Manfred Schmidt-Schauß , Klaus U. Schulz, Solvability of context equations with two context variable is decidable, Journal of Symbolic Computation, v.33 n.1, p.77-122, 01/01/2002
	Antoni Kościelski , Leszek Pacholski, Complexity of Makanin's algorithm, Journal of the ACM (JACM), v.43 n.4, p.670-684, July 1996
	Wojciech Plandowski, Satisfiability of word equations with constants is in NEXPTIME, Proceedings of the thirty-first annual ACM symposium on Theory of computing, p.721-725, May 01-04, 1999, Atlanta, Georgia, United States
	Claudio Gutiérrez, Equations in free semigroups with involution and their relation to equations in free groups, Theoretical Computer Science, v.297 n.1-3, p.271-280, 17 March 2003
	Wojciech Plandowski, Satisfiability of word equations with constants is in PSPACE, Journal of the ACM (JACM), v.51 n.3, p.483-496, May 2004
	J. Beauquier , B. Bérard , L. Fribourg , F. Magniette, Proving convergence of self-stabilizing systems using first-order rewriting and regular languages, Distributed Computing, v.14 n.2, p.83-95, April 2001
	Wojciech Plandowski, An efficient algorithm for solving word equations, Proceedings of the thirty-eighth annual ACM symposium on Theory of computing, May 21-23, 2006, Seattle, WA, USA
	Sergei Vorobyov, Equational theory of context unification is undecidable, Theoretical Computer Science, v.275 n.1-2, p.463-479, March 28 2002
	Jorge Coelho , Mario Florido, XCentric: logic programming for XML processing, Proceedings of the 9th annual ACM international workshop on Web information and data management, November 09-09, 2007, Lisbon, Portugal
	Temur Kutsia, Solving equations with sequence variables and sequence functions, Journal of Symbolic Computation, v.42 n.3, p.352-388, March, 2007
	Temur Kutsia, Flat matching, Journal of Symbolic Computation, v.43 n.12, p.858-873, December, 2008