×

About the Paterson-Wegman linear unification algorithm. (English) Zbl 0645.68103

Summary: The Paterson-Wegman unification algorithm is investigated [cf. M. S. Paterson and M. N. Wegman, ibid. 16, 158-167 (1978; Zbl 0371.68013)]. An error is removed. The proper input format is clarified. A pre-processor is described that associates with each node a list of parent nodes, as required by the core algorithm. A post-processor is described that transforms an ordered substitution, produced by the core algorithm, into a regular substitution, making use of structure sharing when possible. The combination of pre-processor, core algorithm, and post-processor is still a linear algorithm (with respect to the sum of nodes and edges in the input graph).

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68N25 Theory of operating systems
68W99 Algorithms in computer science
68Q25 Analysis of algorithms and problem complexity

Citations:

Zbl 0371.68013
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Wang, C. L.; Lee, R. C.T., Symbolic Logic and Mechanical Theorem Proving (1973), Academic Press: Academic Press New York
[2] Loveland, D. W., Automated Theorem Proving: A Logical Basis (1978), North-Holland: North-Holland Amsterdam · Zbl 0364.68082
[3] Nilsson, N. J., Principles of Artificial Intelligence (1980), Tioga, Palo Alto, Calif. · Zbl 0422.68039
[4] Pattern, M. S.; Wegman, M. N., Linear Unification, (IBM Research Report 5304 (1976), IBM) · Zbl 0365.68042
[5] Paterson, M. S.; Wegman, M. N., Linear unification, (Conference Record of the 8th Annual ACM Symposium on the Theory of Computing (May 1976)), 181-186 · Zbl 0365.68042
[6] Paterson, M. S.; Wegman, M. N., Linear unification, J. Comput. System Sci., 16, No. 2, 158-167 (1978) · Zbl 0371.68013
[7] Robinson, J. A., A machine-oriented logic based on the resolution principle, J. Assoc. Comput. Mach., 12, No. 1, 23-41 (1965) · Zbl 0139.12303
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.