A new approach to universal unfication and its application to AC-unification

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

A complete unification algorithm for simple theories is described. This algorithm is an extension of the variable abstraction approach. Since the associative-commutative (AC) theory is simple, an immediate consequence of this algorithm is a new AC-unification procedure. A partial correctness proof is given and some preliminary termination results for the AC case are presented.

Original languageEnglish (US)
Title of host publication9th International Conference on Automated Deduction, Proceedings
PublisherSpringer Verlag
Pages643-657
Number of pages15
ISBN (Print)9783540193432
DOIs
StatePublished - Jan 1 1988
Event9th International Conference on Automated Deduction, CADE 1988 - Argonne, United States
Duration: May 23 1988May 26 1988

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume310 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other9th International Conference on Automated Deduction, CADE 1988
CountryUnited States
CityArgonne
Period5/23/885/26/88

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A new approach to universal unfication and its application to AC-unification'. Together they form a unique fingerprint.

Cite this