Abstract
The narrowing mechanism has been a major tool in designing complete E-unification procedures for classes of equational theories in the last few years. Meanwhile, it has also been noticed that it is sometimes difficult to build complete procedures using only the narrowing mechanism. This paper analyzes several examples encountered by the authors in the course of research, which show that in certain situations narrowing fails to yield a complete E-unification procedure. Furthermore, we augment the narrowing mechanism with a restricted form of the paramodulation rule. This yields a complete E-unification procedure for all the equational theories that can be described by a confluent term rewriting system. We then present a new procedure in which paramodulation is eliminated by using a set of preconstructed terms, called cover set, which is a substantially reduced set of terms of certain complexity. This provides a degree of completeness, called relative completeness, which is measured by complexity of terms.
Preview
Unable to display preview. Download preview PDF.
References
Brand, D., Proving theorems by the modification method. SIAM J. of Computing, Vol. 4, pp. 412–430, 1975.
Dershowitz, H., Computing with rewrite rules. Information and Control, May/June, 65, 2/3, 1985.
Fay, M.J., First-order unification in an equational theory. in 4th Workshop on Automated Deduction, pp. 161–167, 1979.
Fribourg, L., Oriented equational clauses as a programming language. J. of Logic Programming, Vol 2, pp. 165–177, 1984.
Fribourg, L., A superposition oriented theorem prover. Theoretical Computer Science, Vol. 1, 1985.
Fribourg, L., SLOG: A logic programming language interpreter based on clausal superposition and rewriting. Proc. Symposium on Logic Programming, pp. 172–184, Boston, Mass., July, 1985.
Henschen, L., Private communication, 1985.
Hsiang J. and M. Rusinowitch, A new method for establishing refutational completeness in theorem proving. Proc. of 8th Conference on Automated Deduction, LNCS 230, pp. 141–152, 1986.
Hullot, J.M., Canonical forms and unification. Proc. 5th Conference on Automated Deduction, pp. 318–334, 1980.
Knuth, D. and P. Bendix, Simple word problems in universal algebras. Computational problems in abstract algebra, ed. J. Leech, pp. 163–279, Pergamon Press, 1970.
Loveland, D.W., Automated theorem proving: a logical basis, Norther-Holland, New York, 1978.
O'Donnell, M., Computing in systems described by equations. LNCS 58, Springer-Verlag, New York, 1977.
Peterson, G.E., A technique for establishing completeness results in theorem proving with equality. SIAM J. of Computing, Vol. 12, No. 1, pp.82–100, 1983.
Plotkin, G., Building-in equational theories. Machine Intelligence 7, pp. 73–90, Edinburgh University Press, 1972.
Reddy, U., Narrowing as the operational semantics of functional languages. Proc. Symposium on Logic Programming, pp. 138–151, Boston, Mass., July, 1985.
Robinson, G. and L. Wos, Paramodulation and theorem-proving in first order theories with equality. Machine Intelligence 4, B. Meltzer and D. Michie, eds., Edinburgh University Press, Edinburgh, 1969, pp. 135–150.
Siekmann, J., Universal unification, Proc. 7th International Conference on Automated Deduction, pp. 1–42, Napa, Califomia, May, 1984.
You, J.-H. and P.A. Subrahmanyam, A class of confluent term rewriting systems and unification. J. Automated Reasoning Vol. 2, 391–418, 1986.
You, J.-H., Unification Modulo an Equality Theory for Equational Logic Programming. To appear in J. Computer and System Sciences.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
You, JH., Subrahmanyam, P.A. (1990). On the completeness of narrowing for E-unification. In: Ramani, S., Chandrasekar, R., Anjaneyulu, K.S.R. (eds) Knowledge Based Computer Systems. KBCS 1989. Lecture Notes in Computer Science, vol 444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0018388
Download citation
DOI: https://doi.org/10.1007/BFb0018388
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52850-0
Online ISBN: 978-3-540-47168-4
eBook Packages: Springer Book Archive