FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Formalization of First-Order Syntactic Unification

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

PapersPapers with AbstractsPrefaceAuthor IndexKeyword Index

Paper Information

Title:Formalization of First-Order Syntactic Unification
Authors:Kasper Fabæch Brandt, Anders Schlichtkrull and Jørgen Villadsen
Proceedings:UNIF Extended abstracts
Editors: Mauricio Ayala-Rincon and Philippe Balbiani
Keywords:First-Order Syntactic Unification, Isabelle Proof Assistant, Formalization
Abstract:

ABSTRACT. We present a new formalization in the Isabelle proof assistant of first-order syntactic unification, including a proof of termination.

Pages:7
Talk:Jul 07 17:30 (Session 31S: Nominal Unification and Formalisations)
Paper: