Top

Journal of Automated Reasoning

Published in:

12-08-2022

Faster Linear Unification Algorithm

Author: Dennis de Champeaux

Published in: Journal of Automated Reasoning | Issue 4/2022

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

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.

previous article Fast Left Kan Extensions Using the Chase

next article Pardinus: A Temporal Relational Model Finder

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Available only for authorised users

Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook Of Automated Reasoning. Elsevier, Amsterdam (2001)

de Champeaux, D.: About the Paterson–Wegman linear unification algorithm. J. Comput. Syst. Sci. 32(1), 79–90 (1986). https://doi.org/10.1016/0022-0000(86)90003-6MathSciNetCrossRefMATH

Jacobson, E.: Unification and anti-unification. Technical Report (1991). http://erikjacobsen.com/pdf/unification.pdf

https://github.com/ddccc/Unification. Accessed 24 July 2022

Hoder, K., Voronkov, A.: Comparing unification algorithms in first-order theorem proving. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009: Advances in Artificial Intelligence. Lecture Notes in Computer Science, vol. 5803. Springer, Berlin (2009). https://doi.org/10.1007/978-3-642-04617-9_55CrossRef

Kowalski, R.: A proof procedure using connection graphs. J. Assoc. Comput. Mach. 22(4), 572–659 (1975). https://doi.org/10.1145/321906.321919MathSciNetCrossRefMATH

Martelli, A., Montanari, U.: Unification in linear time and space: a structured presentation. Internal Report B76-16. Ist. di Elaborazione delle Informazione, Consiglio Nazionale delle Ricerche, Pisa, Italy (1976)

Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst. 4(2), 258–282 (1982)CrossRefMATH

Motroi, V., Ciobaco, S.: A Typo in the Paterson–Wegman–de Champeaux algorithm. Arxiv Preprint (2020). https://arxiv.org/abs/2007.00304

10.

Paterson, M.S., Wegman, M.N.: Linear unification. J. Comput. Syst. Sci. 16(2), 158–167 (1978). https://doi.org/10.1016/0022-0000(78)90043-0MathSciNetCrossRefMATH

11.

https://en.wikipedia.org/wiki/Planning_Domain_Definition_Language. Accessed 24 July 2022

12.

Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach. 12(1), 23–41 (1965)MathSciNetCrossRefMATH

13.

https://en.wikipedia.org/wiki/Disjoint-set_data_structure. Accessed 24 July 2022

Title: Faster Linear Unification Algorithm
Author: Dennis de Champeaux
Publication date: 12-08-2022
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 4/2022
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-022-09635-1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 4/2022

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory

Larry Wos: Visions of Automated Reasoning

Fast Left Kan Extensions Using the Chase

A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column

Tuple Interpretations for Termination of Term Rewriting

Set of Support, Demodulation, Paramodulation: A Historical Perspective

Premium Partner