Skip to main content
Erschienen in: Journal of Automated Reasoning 4/2022

12.08.2022

Faster Linear Unification Algorithm

verfasst von: Dennis de Champeaux

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2022

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

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!

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!

Anhänge
Nur mit Berechtigung zugänglich
Literatur
1.
Zurück zum Zitat Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook Of Automated Reasoning. Elsevier, Amsterdam (2001) Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook Of Automated Reasoning. Elsevier, Amsterdam (2001)
7.
Zurück zum Zitat 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.: 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)
8.
Zurück zum Zitat Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst. 4(2), 258–282 (1982)CrossRefMATH Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst. 4(2), 258–282 (1982)CrossRefMATH
12.
Metadaten
Titel
Faster Linear Unification Algorithm
verfasst von
Dennis de Champeaux
Publikationsdatum
12.08.2022
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 4/2022
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-022-09635-1

Weitere Artikel der Ausgabe 4/2022

Journal of Automated Reasoning 4/2022 Zur Ausgabe

OriginalPaper

A Wos Challenge Met

Premium Partner