# An Efficient Unification Algorithm

@article{Martelli1982AnEU, title={An Efficient Unification Algorithm}, author={Alberto Martelli and Ugo Montanari}, journal={ACM Trans. Program. Lang. Syst.}, year={1982}, volume={4}, pages={258-282} }

The unification problem in f'mst-order predicate calculus is described in general terms as the solution of a system of equations, and a nondeterministic algorithm is given. [...] Key Method A new unification algorithm, characterized by having the acyclicity test efficiently embedded into it, is derived from the nondeterministic one, and a PASCAL implementation is given. A comparison with other well-known unification algorithms shows that the algorithm described here performs well in all cases. Expand

#### Topics from this paper

#### 892 Citations

A Unification Algorithm for Infinite Trees

- Computer Science
- IJCAI
- 1983

A simple unification algorithm for infinite trees has been developed. The algorithm is designed to work efficiently under structure sharing implementations of logic programming languages, e.g.,… Expand

Unification in a Combination of Equational Theories: an Efficient Algorithm

- Mathematics, Computer Science
- CADE
- 1990

An algorithm is presented for solving equations in a combination of arbitrary theories with disjoint sets of function symbols that consists in a set of transformation rules that simplify a unification problem until a solved form is obtained. Expand

A Unification Algorithms for Confluent Theories

- Computer Science
- ICALP
- 1987

A correct and complete unification algorithm for confluent theories that is demand driven and can handle infinite and partial instantiated objects and thus can be used as a means to integrate functional and logic programming. Expand

On the termination of an algorithm for unification in equational theories

- Mathematics
- Fourth IEEE Region 10 International Conference TENCON
- 1989

The termination properties of a semantic unification procedure for the problem t=/sub R/t' are studied, where R is expressed by means of a canonical term rewriting system and t' is a round term not… Expand

Lazy Unification with Inductive Simplification

- Computer Science
- WLP
- 1993

This paper presents an improvement of the proposed lazy unification methods by incorporating simplification with inductive axioms into the unification process, and proves soundness and completeness of the method for equational theories represented by ground confluent and terminating rewrite systems. Expand

Lazy Unification with Simplification

- Computer Science
- ESOP
- 1994

This paper presents an improvement of the proposed lazy unification methods by incorporating simplification into the unification process, since simplification is a deterministic computation process, more efficient unification algorithms can be achieved. Expand

Implementation of a UU-Algorithm for Primitive Recursive Tree Functions

- Computer Science
- FCT
- 1995

We present the implementation of an efficient universal unification algorithm for the class of equational theories which are induced by primitive recursive tree functions, on an abstract machine and… Expand

A New Approach to Universal Unification and Its Application to AC-Unification

- Mathematics, Computer Science
- CADE
- 1988

A complete unification algorithm for simple theories is described and a partial correctness proof is given and some preliminary termination results for the AC case are presented. Expand

A Categorical Unification Algorithm

- Computer Science
- CTCS
- 1985

This is a case study in the design of computer programs based upon the twin themes of abstraction and constructivity and considers the unification of a symbol-manipulative task and derives a unification algorithm based upon constructions in category theory. Expand

Unification in an Algebra With Choice and Action Prefix

- Mathematics
- 1994

This paper contains a uniication algorithm for a restricted process algebra with as only operators nondeterministic choice and unary action preex-operators, and with innnite processes. Termination is… Expand

#### References

SHOWING 1-10 OF 42 REFERENCES

A Unification Algorithm for Typed lambda-Calculus

- Computer Science, Mathematics
- Theor. Comput. Sci.
- 1975

It is shown that the search space for unification of formulas in typed ω -order λ -calculus is significantly smaller than the one for finding the most general unifiers, and its correctness is proved. Expand

A Complete Unification Algorithm for Associative-Commutative Functions

- Mathematics, Computer Science
- IJCAI
- 1975

An algorithm which unifies terms whose function is associativa and commutative is presented here and returns a complete set of unifiers without recourse to the indefinite generation of vurianU and instances of the terms being unified required by previous solutions to the problem. Expand

Complexity of the unification algorithm for first-order expressions

- Mathematics
- 1975

Rewriting and comparisons are the complexity aspects of the unification algorithm which are considered in this paper. A simplified version of Robinson's algorithm [2] is described where rewriting… Expand

Linear unification

- Mathematics, Computer Science
- STOC '76
- 1976

A unification algorithm is described which tests a set of expressions for unifiability and which requires time and space which are only linear in the size of the input.

A Machine-Oriented Logic Based on the Resolution Principle

- Computer Science
- JACM
- 1965

The paper concludes with a discussion of several principles which are applicable to the design of efficient proof-procedures employing resolution as the basle logical process. Expand

Ttle sharing of structure in theorem proving programs

- Computer Science
- 1972

The concept of the value of an expression in a binding environment which is used to standardize clauses apart and share the structure of parents in representing the resolvent in resolution programs is introduced. Expand

A Theory of Type Polymorphism in Programming

- Computer Science
- J. Comput. Syst. Sci.
- 1978

This work presents a formal type discipline for polymorphic procedures in the context of a simple programming language, and a compile time type-checking algorithm w which enforces the discipline. Expand

A Transformation System for Developing Recursive Programs

- Computer Science
- J. ACM
- 1977

A system of rules for transforming programs is described, with the programs in the form of recursion equations. An initially very simple, lucid, and hopefully correct program is transformed into a… Expand

Theorem Proving with Structure Sharing and Efficient Unification

- Mathematics, Computer Science
- IJCAI
- 1977

A careful complexity analysis may help in improving substantially the performance of proof checkers and a powerful logic formalism and an efficient proof checker can allow to prove manually theorems whose automatic proof would be otherwise very far from the state of the art. Expand

Prolog - the language and its implementation compared with Lisp

- Computer Science
- 1977

It is argued that pattern matching is a better method for expressing operations on structured data than conventional selectors and constructors - both for the user and for the implementor. Expand