| dc.rights.license | CC-BY-NC-ND | |
| dc.contributor.advisor | Van Oostrom, Vincent | |
| dc.contributor.advisor | Visser, Albert | |
| dc.contributor.author | Bitane, Y. | |
| dc.date.accessioned | 2015-10-06T17:01:31Z | |
| dc.date.available | 2015-10-06T17:01:31Z | |
| dc.date.issued | 2015 | |
| dc.identifier.uri | https://studenttheses.uu.nl/handle/20.500.12932/27889 | |
| dc.description.abstract | Confluence is an important property of term rewriting systems. Since any algorithm can be modelled as such, the decreasing diagrams technique is very useful for establishment of this property. Van Oostrom has further refined the technique by means of the decreasing proof order in his 2012 article. We have formalized the main two lemmas of this method, thereby verifying its correctness. | |
| dc.description.sponsorship | Utrecht University | |
| dc.format.extent | 963965 | |
| dc.format.mimetype | application/pdf | |
| dc.language.iso | en | |
| dc.title | On Formalizing Decreasing Proof Orders | |
| dc.type.content | Master Thesis | |
| dc.rights.accessrights | Open Access | |
| dc.subject.keywords | term rewriting, coq, automated theorem proving, decreasing diagrams | |
| dc.subject.courseuu | Cognitive Artificial Intelligence | |
