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

Mark Franzen; Lawrence Joseph Henschen

doi:10.1007/BFb0012863

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

Mark Franzen, Lawrence Joseph Henschen

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	9th International Conference on Automated Deduction, Proceedings
Editors	Ewing Lusk, Ross Overbeek
Publisher	Springer Verlag
Pages	643-657
Number of pages	15
ISBN (Print)	9783540193432
DOIs	https://doi.org/10.1007/BFb0012863
State	Published - 1988
Event	9th International Conference on Automated Deduction, CADE 1988 - Argonne, United States Duration: May 23 1988 → May 26 1988

Publication series

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

Other

Other	9th International Conference on Automated Deduction, CADE 1988
Country/Territory	United States
City	Argonne
Period	5/23/88 → 5/26/88

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/BFb0012863

Cite this

Franzen, M., & Henschen, L. J. (1988). A new approach to universal unfication and its application to AC-unification. In E. Lusk, & R. Overbeek (Eds.), 9th International Conference on Automated Deduction, Proceedings (pp. 643-657). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 310 LNCS). Springer Verlag. https://doi.org/10.1007/BFb0012863

Franzen, Mark ; Henschen, Lawrence Joseph. / A new approach to universal unfication and its application to AC-unification. 9th International Conference on Automated Deduction, Proceedings. editor / Ewing Lusk ; Ross Overbeek. Springer Verlag, 1988. pp. 643-657 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{3b7730aa550344779ccc01d03a25383c,

title = "A new approach to universal unfication and its application to AC-unification",

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.",

author = "Mark Franzen and Henschen, {Lawrence Joseph}",

note = "Publisher Copyright: {\textcopyright} 1988, Springer-Verlag.; 9th International Conference on Automated Deduction, CADE 1988 ; Conference date: 23-05-1988 Through 26-05-1988",

year = "1988",

doi = "10.1007/BFb0012863",

language = "English (US)",

isbn = "9783540193432",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "643--657",

editor = "Ewing Lusk and Ross Overbeek",

booktitle = "9th International Conference on Automated Deduction, Proceedings",

}

Franzen, M & Henschen, LJ 1988, A new approach to universal unfication and its application to AC-unification. in E Lusk & R Overbeek (eds), 9th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 310 LNCS, Springer Verlag, pp. 643-657, 9th International Conference on Automated Deduction, CADE 1988, Argonne, United States, 5/23/88. https://doi.org/10.1007/BFb0012863

A new approach to universal unfication and its application to AC-unification. / Franzen, Mark; Henschen, Lawrence Joseph.
9th International Conference on Automated Deduction, Proceedings. ed. / Ewing Lusk; Ross Overbeek. Springer Verlag, 1988. p. 643-657 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 310 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Franzen, Mark

AU - Henschen, Lawrence Joseph

PY - 1988

Y1 - 1988

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84934868020&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84934868020&partnerID=8YFLogxK

U2 - 10.1007/BFb0012863

DO - 10.1007/BFb0012863

M3 - Conference contribution

AN - SCOPUS:84934868020

SN - 9783540193432

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 643

EP - 657

BT - 9th International Conference on Automated Deduction, Proceedings

A2 - Lusk, Ewing

A2 - Overbeek, Ross

PB - Springer Verlag

T2 - 9th International Conference on Automated Deduction, CADE 1988

Y2 - 23 May 1988 through 26 May 1988

ER -

Franzen M, Henschen LJ. A new approach to universal unfication and its application to AC-unification. In Lusk E, Overbeek R, editors, 9th International Conference on Automated Deduction, Proceedings. Springer Verlag. 1988. p. 643-657. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/BFb0012863

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

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this