17 citations · 51 across the 10 of their papers we have counts for
Showing 2012Show all
3 papers · 1 filter
cs.LO2012★ 1 cited
Confluence by Decreasing Diagrams -- Formalized
Harald Zankl
This paper presents a formalization of decreasing diagrams in the theorem prover Isabelle. It discusses mechanical proofs showing that any locally decreasing abstract rewrite syste…
cs.LO2012★ 3 cited
Recording Completion for Finding and Certifying Proofs in Equational Logic
Thomas Sternagel, René Thiemann, Harald Zankl +1
When we want to answer/certify whether a given equation is entailed by an equational system we face the following problems: (1) It is hard to find a conversion (but easy to certify…
cs.LO2012★ 1 cited
CeTA - A Tool for Certified Termination Analysis
Christian Sternagel, René Thiemann, Sarah Winkler +1
Since the first termination competition in 2004 it is of great interest, whether a proof that has been automatically generated by a termination tool, is indeed correct. The increas…