A practically efficient and almost linear unification algorithm (Q1105360)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: A practically efficient and almost linear unification algorithm |
scientific article; zbMATH DE number 4058850
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A practically efficient and almost linear unification algorithm |
scientific article; zbMATH DE number 4058850 |
Statements
A practically efficient and almost linear unification algorithm (English)
0 references
1988
0 references
An efficient unification algorithm for first-order terms is described. It relies on the known theoretical framework of homogeneous and valid equivalence relations on terms and it makes use of a union-find algorithmic schema, thus keeping an almost linear worst-case complexity. Its advantages over similar algorithms are a very low overhead and practical efficiency, even for small terms, that are due to simple data structures and careful design tradeoffs. The proposed algorithm is described in detail such as to be easily implemented. Its main part is proved, and its complexity analyzed. Comparative experimental results that support its advantage are given.
0 references
efficient unification algorithm
0 references
first-order terms
0 references
almost linear worst- case complexity
0 references
0 references
0.92128235
0 references
0.91044456
0 references
0 references
0.9073377
0 references
0.89886224
0 references
0 references
0.8708871
0 references
