AFP
2015
Springer
8 years 22 days ago
2015
Springer
Isabelle/Isar provides named cases to structure proofs. This article contains an implementation of a proof method casify, which can be used to easily extend proof tools with suppo...
AFP
2015
Springer
8 years 22 days ago
2015
Springer
This theory formalizes a commutation version of decreasing diagrams for Church-Rosser modulo. The proof follows Felgenhauer and van Oostrom (RTA 2013). The theory also provides im...
AFP
2015
Springer
8 years 22 days ago
2015
Springer
Encodings or the proof of their absence are the main way to compare process calculi. To analyse the quality of encodings and to rule out trivial or meaningless encodings, they are...
AFP
2015
Springer
8 years 22 days ago
2015
Springer
Matrix interpretations are useful as measure functions in termination proving. In order to use these interpretations also for complexity analysis, the growth rate of matrix powers...
AFP
2015
Springer
8 years 22 days ago
2015
Springer
In this work, we prove the lower bound ln(Hn)−ln(5 3 ) for the partial sum of the Prime Harmonic series and, based on this, the divergence of the Prime Harmonic Series n p=1[p p...
AFP
2015
Springer
8 years 22 days ago
2015
Springer
Based on existing libraries for matrices, factorization of rational polynomials, and Sturm’s theorem, we formalized algebraic numbers in Isabelle/HOL. Our development serves as ...
AFP
2015
Springer
8 years 22 days ago
2015
Springer