Abstract
In various fields using first order terms — like automated reasoning, logic programming or term rewriting — we encounter infinite sequences of structurally similar terms, leading to non-terminating or at least time and space consuming computations. As a remedy we introduce a meta-language consisting of recursive terms (R-terms), which are a finite representation of infinite sets of terms.
Given two R-terms r 1 and r 2 there may be infinitely many most general unifiers between those terms represented by r 1 and those represented by r 2. We present a unification algorithm for R-terms, which computes all first order unifiers simultaneously and yields a finite and complete representation for the potentially infinite set of first order unifiers.
We demonstrate the practicability of our approach by applying R-terms and meta-unification to automated theorem proving, logic programming and cycle unification.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
W. Bibel, S. Hölldobler and J. Würtz. Cycle Unification. Forschungsbericht AIDA-91-15, TH Darmstadt, 1991.
M. Clausen and A. Fortenbacher. Efficient Solution of Linear Diophantine Equations. J. Symbolic Computation 8 (1989), 201–216.
H. Chen and J. Hsiang. Logic Programming with Recurrence Domains. ICALP '91, LNCS 510 (1991), 20–34.
P. Devienne. Weighted graphs: a tool for studying the halting problem and time complexity in term rewriting systems and logic programming. Theoretical Computer Science 75 (1990), 157–215.
H. Kirchner. Schematization of infinite sets of rewrite rules generated by divergent completion processes. Theoretical Computer Science 67 (1989), 303–332.
D. Lankford. Non-negative Integer Basis Algorithms for Linear Equations with Integer Coefficients. J. Automated Reasoning 5 (1989), 25–35.
D. McAllester. Grammar Rewriting. CADE-11, to appear in LNCS, (1992).
A. Martelli and U. Montanari. An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems, Vol. 4 No. 2 (1982), 258–282.
H. J. Ohlbach. Compilation of recursive two-literal clauses into unification algorithms. Proc. of the AIMSA (P. Jorrand and V. Sgurev, eds.), 13–22, 1990.
J. A. Robinson. Automatic Deduction with Hyper-Resolution. Int. J. Comput. Math. 1 (1965), 227–234.
G. Salzer. Unification of Meta-Terms. Dissertation, Techn. Univ. Wien, 1991.
G. Salzer. The Unification of Infinite Sets of Terms and its Applications. Technical Report E185-2/S05, Technische Universität Wien, 1992.
D. Schreye, M. Bruynooghe, K. Verschaetse. On the Existence of Nonterminating Queries for a Restricted Class of Prolog-Clauses. Artificial Intelligence 41 (1989/90), 237–248.
J. Würtz. Unifying Cycles. Forschungsbericht, DFKI Saarbrücken, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Salzer, G. (1992). The unification of infinite sets of terms and its applications. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1992. Lecture Notes in Computer Science, vol 624. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013079
Download citation
DOI: https://doi.org/10.1007/BFb0013079
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55727-2
Online ISBN: 978-3-540-47279-7
eBook Packages: Springer Book Archive