Anzeige
Erschienen in:
12.08.2022
Faster Linear Unification Algorithm
Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2022
Einloggen, um Zugang zu erhaltenAbstract
The Robinson unification algorithm has exponential worst case behavior. This triggered the development of (semi-)linear versions around 1976 by Martelli and Montanari as well as by Paterson and Wegman (J Comput Syst Sci 16(2):158–167, 1978, https://doi.org/10.1016/0022-0000(78)90043-0). Another version emerged by Baader and Snyder around 2001. While these versions are distinctly faster on larger input pairs, the Robinson version still does better than them on small-sized inputs. This paper describes yet another (semi-)linear version that is faster and challenges also the Robinson version on small-sized inputs. All versions have been implemented and compared against each other on different types and sizes of input pairs.