Minimal and complete word unification
- 3 January 1990
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 37 (1) , 47-85
- https://doi.org/10.1145/78935.78938
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.Keywords
This publication has 4 references indexed in Scilit:
- Universal unification and a classification of equational theoriesPublished by Springer Nature ,2005
- THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUPMathematics of the USSR-Sbornik, 1977
- A Human Oriented Logic for Automatic Theorem-ProvingJournal of the ACM, 1974
- CRT-AIDED SEMI-AUTOMATED MATHEMATICSPublished by Defense Technical Information Center (DTIC) ,1967