On Formalizing Decreasing Proof Orders
Publication date
Authors
DOI
Document Type
Master Thesis
Metadata
Show full item recordCollections
License
CC-BY-NC-ND
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.
Keywords
term rewriting, coq, automated theorem proving, decreasing diagrams