Formalization of a near-linear time algorithm for solving the unification problem |
Kasper F. Brandt
|
| Abstract | This thesis deals with formal verification of an imperatively formulated algorithm for solving first-order syntactic unification based on sharing of terms by storing them in a DAG. A theory for working with the relevant data structures is developed and a part of the algorithm is shown equivalent with a functional formulation. |
| Type | Master's thesis [Academic thesis] |
| Year | 2018 |
| 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.-2018 |
| Note | |
| Electronic version(s) | [pdf] |
| Publication link | http://www.compute.dtu.dk/english |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |