Formalization of First-Order Syntactic Unification

Kasper Fabæch Brandt, Anders Schlichtkrull, Jørgen Villadsen

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

154 Downloads (Pure)

Abstract

We present a new formalization in the Isabelle proof assistant of first-order syntactic unification, including a proof of termination. Our formalization follows, almost down to the letter, the ML-code from Baader and Nipkow's book "Term Rewriting and All That" (1998). Correctness is implied by the formalization's similarity to Baader and Nipkow's ML-code, but we have yet to formalize the correctness of the unification algorithm.
Original languageEnglish
Title of host publication32nd International Workshop on Unification (UNIF 2018) — Informal Proceedings
Number of pages7
PublisherThe International Unification Workshop (UNIF)
Publication date2018
Article numberP9
Publication statusPublished - 2018
Event32nd International Workshop on Unification - Oxford, United Kingdom
Duration: 7 Jul 20187 Jul 2018

Conference

Conference32nd International Workshop on Unification
CountryUnited Kingdom
CityOxford
Period07/07/201807/07/2018

Cite this

Brandt, K. F., Schlichtkrull, A., & Villadsen, J. (2018). Formalization of First-Order Syntactic Unification. In 32nd International Workshop on Unification (UNIF 2018) — Informal Proceedings [P9] The International Unification Workshop (UNIF). http://unif2018.cic.unb.br/