(Nominal) unification by recursive descent with triangular substitutions

Ramana Kumar; Michael Norrish

doi:10.1007/978-3-642-14052-5_6

(Nominal) unification by recursive descent with triangular substitutions

Ramana Kumar^*, Michael Norrish

^*Corresponding author for this work

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

15 Citations (Scopus)

Abstract

Using HOL4, we mechanise termination and correctness for two unification algorithms, written in a recursive descent style. One computes unifiers for first order terms, the other for nominal terms (terms including α-equivalent binding structure). Both algorithms work with triangular substitutions in accumulator-passing style: taking a substitution as input, and returning an extension of that substitution on success.

Original language	English
Title of host publication	Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings
Pages	51-66
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-14052-5_6
Publication status	Published - 2010
Event	1st International Conference on Interactive Theorem Proving, ITP 2010 - Edinburgh, United Kingdom Duration: 11 Jul 2010 → 14 Jul 2010

Publication series

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

Conference

Conference	1st International Conference on Interactive Theorem Proving, ITP 2010
Country/Territory	United Kingdom
City	Edinburgh
Period	11/07/10 → 14/07/10

Access to Document

10.1007/978-3-642-14052-5_6

Cite this

Kumar, R., & Norrish, M. (2010). (Nominal) unification by recursive descent with triangular substitutions. In Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings (pp. 51-66). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6172 LNCS). https://doi.org/10.1007/978-3-642-14052-5_6

@inproceedings{6c7b873dfabe483ba0db64a463fc8646,

title = "(Nominal) unification by recursive descent with triangular substitutions",

abstract = "Using HOL4, we mechanise termination and correctness for two unification algorithms, written in a recursive descent style. One computes unifiers for first order terms, the other for nominal terms (terms including α-equivalent binding structure). Both algorithms work with triangular substitutions in accumulator-passing style: taking a substitution as input, and returning an extension of that substitution on success.",

author = "Ramana Kumar and Michael Norrish",

year = "2010",

doi = "10.1007/978-3-642-14052-5_6",

language = "English",

isbn = "3642140513",

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

pages = "51--66",

booktitle = "Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings",

note = "1st International Conference on Interactive Theorem Proving, ITP 2010 ; Conference date: 11-07-2010 Through 14-07-2010",

}

Kumar, R & Norrish, M 2010, (Nominal) unification by recursive descent with triangular substitutions. in Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6172 LNCS, pp. 51-66, 1st International Conference on Interactive Theorem Proving, ITP 2010, Edinburgh, United Kingdom, 11/07/10. https://doi.org/10.1007/978-3-642-14052-5_6

(Nominal) unification by recursive descent with triangular substitutions. / Kumar, Ramana; Norrish, Michael.
Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings. 2010. p. 51-66 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6172 LNCS).

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

TY - GEN

T1 - (Nominal) unification by recursive descent with triangular substitutions

AU - Kumar, Ramana

AU - Norrish, Michael

PY - 2010

Y1 - 2010

N2 - Using HOL4, we mechanise termination and correctness for two unification algorithms, written in a recursive descent style. One computes unifiers for first order terms, the other for nominal terms (terms including α-equivalent binding structure). Both algorithms work with triangular substitutions in accumulator-passing style: taking a substitution as input, and returning an extension of that substitution on success.

AB - Using HOL4, we mechanise termination and correctness for two unification algorithms, written in a recursive descent style. One computes unifiers for first order terms, the other for nominal terms (terms including α-equivalent binding structure). Both algorithms work with triangular substitutions in accumulator-passing style: taking a substitution as input, and returning an extension of that substitution on success.

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

U2 - 10.1007/978-3-642-14052-5_6

DO - 10.1007/978-3-642-14052-5_6

M3 - Conference contribution

SN - 3642140513

SN - 9783642140518

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

SP - 51

EP - 66

BT - Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings

T2 - 1st International Conference on Interactive Theorem Proving, ITP 2010

Y2 - 11 July 2010 through 14 July 2010

ER -

(Nominal) unification by recursive descent with triangular substitutions

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this