Kai Brünnler Livres

This book constitutes the refereed proceedings of the 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011, held in Bern, Switzerland, in July 2011. The 16 revised research papers presented together with 2 system descriptions were carefully reviewed and selected from 34 submissions. The papers cover many topics in the wide range of applications of tableaux and related methods such as analytic tableaux for various logics, related techniques and concepts, related methods, new calculi and methods for theorem proving in classical and non-classical logics, as well as systems, tools, implementations and applications; all with a special focus on hardware and software verifications, semantic technologies, and knowledge engineering.

In this thesis we see deductive systems for classical propositional and predicate logic which use deep inference, i. e. inference rules apply arbitrarily deep inside formulas, and a certain symmetry, which provides an involution on derivations. Like sequent systems, they have a cut rule which is admissible. Unlike sequent systems, they enjoy various new interesting properties. Not only the identity axiom, but also cut, weakening and even contraction are reducible to atomic form. This leads to inference rules that are local, meaning that the effort of applying them is bounded, and finitely generating, meaning that, given a conclusion, there is only a finite number of premises to choose from. The systems also enjoy new normal forms for derivations and, in the propositional case, a cut elimination procedure that is drastically simpler than the ones for sequent systems.

Der Begriff Blockchain steht für einen technologischen Durchbruch auf dem Gebiet digitaler Währungen. Das Konzept hinter diesem Begriff ist allerdings nicht einfach zu verstehen. Eine Blockchain ist eine Datenstruktur, die in kryptografischen Protokollen eingesetzt wird, um Sicherheit gegen bestimmte Angriffe zu gewährleisten. Ihr Sinn erschließt sich nur dann, wenn man diese Angriffe durchdacht hat. Nach einer kurzen Erläuterung der kryptografischen Grundlagen wird in diesem Buch deshalb der Aufbau eines Blockchain-basierten Protokolls von Grund auf nachvollzogen. Ausgehend von einem Protokoll, das jeder kennt, der schon einmal E-Banking benutzt hat, werden Schritt für Schritt Probleme aufgezeigt und gelöst und dabei neue Protokolle entwickelt – bis hin zu einer Blockchain. Abschließend werden mit dem gewonnenen Verständnis Anwendungsfälle von Blockchains identifiziert und auch ausgeschlossen. Sie lernen ausgewählte Blockchain-Anwendungen wie z. B. Zeitstempel für Dokumente, fälschungssichere Logs und verifizierbare Zufallszahlen kennen.