Formalized Unification Algorithms |
Kristoffer Hvidtfeldt
|
| Abstract | The goal of the thesis is to implement a unification algorithm from the book "Term rewriting and all that" in the theorem prover Isabelle/HOL, so that proofs of termination and correctness can be formalized. In doing so the unification algorithm will be analyzed and compared to more traditional algorithms.
It will also give an opportunity to look at the challenges which arises when implementing, proving and the formalizations of algorithms in Isabelle/HOL. |
| Type | Master's thesis [Academic thesis] |
| Year | 2017 |
| Publisher | Technical University of Denmark, Department of Applied Mathematics and Computer Science |
| Address | Richard Petersens Plads, Building 324, DK-2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk |
| Series | DTU Compute M.Sc.-2017 |
| Note | |
| Electronic version(s) | [pdf] |
| Publication link | http://www.compute.dtu.dk/English.aspx |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |