Sciweavers

Share
AFP
2015
Springer
4 years 2 months ago
Euler's Partition Theorem
Euler’s Partition Theorem states that the number of partitions with only distinct parts is equal to the number of partitions with only odd parts. The combinatorial proof follows...
Lukas Bulwahn
AFP
2015
Springer
4 years 2 months ago
The Generic Unwinding Theorem for CSP Noninterference Security
The classical definition of noninterference security for a deterministic state machine with outputs requires to consider the outputs produced by machine actions after any trace, ...
Pasquale Noce
AFP
2015
Springer
4 years 2 months ago
Generating Cases from Labeled Subgoals
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...
Lars Noschinski
AFP
2015
Springer
4 years 2 months ago
Decreasing Diagrams II
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...
Bertram Felgenhauer
AFP
2015
Springer
4 years 2 months ago
Analysing and Comparing Encodability Criteria for Process Calculi
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...
Kirstin Peters, Rob J. van Glabbeek
AFP
2015
Springer
4 years 2 months ago
Matrices, Jordan Normal Forms, and Spectral Radius Theory
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...
René Thiemann, Akihisa Yamada 0002
AFP
2015
Springer
4 years 2 months ago
The Divergence of the Prime Harmonic Series
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...
Manuel Eberl
AFP
2015
Springer
4 years 2 months ago
Algebraic Numbers in Isabelle/HOL
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 ...
René Thiemann, Akihisa Yamada 0002
AHSWN
2016
4 years 3 months ago
Latency Analysis for M2M and Online Gaming Traffic in an HSPA Network
This paper analyzes latency in a High-Speed Packet Access network appropriately resourced for emulated Machine-to-Machine and Online Gaming traffic. Transmission Control Protocol (...
Milica Popovic, Dejan Drajic, Philipp Svoboda, Nav...
books