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

329 Downloads (Pure)


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


Conference32nd International Workshop on Unification
Country/TerritoryUnited Kingdom


Dive into the research topics of 'Formalization of First-Order Syntactic Unification'. Together they form a unique fingerprint.

Cite this