Hauptseite | Programm | Anfahrt
Module für Beweissprachen
Die Theoriesammlungen interaktiver Beweiser haben über die letzten Jahre beachtlichen Umfang angenommen. Ähnlich wie bei Programmiersprachen wird der Einsatz von Modulsystemen erforderlich. Wir stellen Locales, das Modulsystem von Isabelle, vor. Spezielle Anforderungen, die sich aus dem Beweiserkontext und der Einbindung in die Beweissprache Isar ergeben, führen dazu, daß sich das Modulkonzept deutlich von dem in Programmiersprachen unterscheidet.
Textbook Proofs Meet Formal Logic --- The Problem of Underspecification and Granularity
Unlike computer algebra systems, automated theorem provers have not yet achieved considerable recognition and relevance in mathematical practice. A significant shortcoming of mathematical proof assistance systems is that they require the fully formal representation of mathematical content, whereas in mathematical practice an informal, natural-language-like representation where obvious parts are omitted is common. We aim to support mathematical paper writing by integrating a scientific text editor and mathematical assistance systems such that mathematical derivations authored by human beings in a mathematical document can be automatically checked. To this end, we first define a calculus-independent representation language for formal mathematics that allows for underspecified parts. Then we provide two systems of rules that check if a proof is correct and at an acceptable level of granularity. These checks are done by decomposing the proof into basic steps that are then passed on to proof assistance systems for formal verification. We illustrate our approach using an example textbook proof.
Automatisches Beweisen bei der Erkennung semantischer Fehler in SQL-Anfragen
Eine SQL-Anfrage enthält einen semantischen Fehler, wenn sie zwar syntaktisch korrekt ist, aber nicht (oder nicht immer) das beabsichtigte Ergebnis liefert. Zum Teil gibt es auch ohne Kenntnis der Aufgabe recht starke Indizien für einen semantischen Fehler. Zum Beispiel sind in Klausuren zu Datenbank-Vorlesungen selbst inkonsistente Bedingungen nicht selten. Im Vortrag wird eine Übersicht über weitere Fehlertypen mit Angaben zur Häfigkeit in Klausuren gegeben. Die Erkennung vieler dieser Fehler lässt sich auf einen Konsistenztest zurückführen.
Obwohl SQL eine deklarative Sprache ist, sind Laufzeitfehler bei der Ausführung von SQL-Anfragen möglich. Für sichere Software wäre es nun gut, zu beweisen, daß solche Fehler bei den gegebenen Anfragen niemals auftreten können. Auch dieses Problem benötigt einen Konsistenztest.
Im letzten Teil des Vortrags wird der im aktuellen Prototyp des Werkzeugs "SQLlint" verwendete einfache Konsistenztest skizziert.
Formal Verification of an Off-Line Result Checker for Priority Queues
We describe how we formally verified the result checker for priority queues that is implemented in LEDA. A result checker of a datastructure is a second datastructure that checks all input and output of the first datastructure, and which is able to detect when the first datastructure makes a mistake. We have developed a formalism, based on the notion of implementation, which links abstract specifications to concrete implementations. The method allows non-determinism in the abstract specifications that can be filled in by the concrete implementation. Using this formalism, we have formally verified that, if the checker has not reported an error up to a certain moment, then the structure it checks has behaved like a priority queue up to that moment. For the verification, we made use of the first-order theorem prover Saturate.
(This talk is based on joint work with Ruzica Piskac)
Proving and Disproving Termination of TRSs using the Dependency Pair Framework
The dependency pair approach is one of the most powerful techniques for automated termination proofs of term rewrite systems. Up to now, it was regarded as one of several possible methods to prove termination. We show that dependency pairs can instead be used as a general concept to integrate arbitrary techniques for termination analysis. In this way, the benefits of different techniques can be combined and their modularity and power are increased significantly. We refer to this new concept as the dependency pair framework to distinguish it from the old dependency pair approach. We also demonstrate how to prove non-termination with the framework, while up to now dependency pairs were only used to verify termination. The dependency pair framework and all techniques presented are implemented in the automated termination prover AProVE.
This is joint work with Jürgen Giesl and Peter Schneider-Kamp.
Ein ASM-basierter Ansatz zur Verifikation von Sicherheitsprotokollen
Sichere Kommunikation ist in vielen E-Commerce Anwendungen von zentraler Bedeutung. In den Anwendungen werden höchst vertrauliche Informationen übertragen, wie z.B. die persönlichen Kundendaten oder auch digitale Repräsentanten von Wirtschaftsgütern, z.B. Geld oder Flugtickets. Die Kommunikation wird dabei im Allgemeinen durch kryptographische Protokolle, auch Sicherheitsprotokolle genannt, geschützt.
Es ist ein bekanntes Problem, daß der Entwurf sicherer kryptographischer Protokolle schwierig ist. Oftmals enthalten scheinbar gute Protokolle subtile Fehler und ermöglichen unerwartete Effekte. Zur Qualitätssicherung der Protokolle kommen daher formale Methoden zum Einsatz, die einen strengen Beweis erlauben, daß die Protokolle den gewünschten Sicherheitseigenschaften genügen.
In meinem Vortrag präsentiere ich einen Ansatz zur Modellierung und Verifikation von Sicherheitsprotokollen für E-Commerce Anwendungen. Der Modellierungsansatz kombiniert algebraische Spezifikationen zur Datenmodellierung mit einer Abstract State Machine (ASM) zur Beschreibung der dynamischen Aspekte der Protokolle. Die ASM ist ein Programm, das alle in der Anwendung möglichen Abläufe erzeugen kann. Für den Nachweis der Sicherheit einer Applikation ist die Beweisverpflichtung zu zeigen, daß die ASM solche Zustände, in denen eine Sicherheitseigenschaft verletzt wird, nicht erreicht. Die ASM wird als Programm in der Dynamischen Logik (DL) des KIV-Systems formuliert, Beweise über die ASM werden mit dem KIV-System geführt. Zur Illustration des Ansatzes präsentiere ich auch eine kleine Anwendung, einen Chipkarten-basierten elektronischen Geldbeutel.
KRHyper --- In Your Pocket
Adapting DPLL for the Computation of Propositional Forgetting
The forget operation (or predicate quantifier elimination, or computation of uniform interpolants) has applications such as partitioning and preprocessing of knowledge bases, distributed exchange of knowledge, integration and adaption of knowledge bases, computation of circumscription and maintenance of knowledge bases for planning. Further applications are in model-based diagnosis, correspondence theory for modal logics and circuit compilation.
The Davis Putnam Logemann Loveland method (DPLL) with certain refinements, especially dependency directed backjumping, is the basis for state of the art satisfiability solvers and also knowledge compilers. Only recently a specification of DPLL as a calculus has been given, which takes into account refinements essential for its success (Abstract DPLL by Nieuwenhuis, Oliveras and Tinelli). We extend this specification of DPLL and show how derivates of a refined DPLL can be used for model generation, the computation of certain formula transformations and forgetting for propositional logic.
Model-Generation Theorem Proving for First-Order Logic Ontologies
Formal ontologies play an increasingly important role in demanding knowledge representation applications like the Semantic Web. Automated reasoning support for these ontologies is mandatory for tasks like debugging, classifying or querying the knowledge bases, and description logic (DL) reasoners have been shown to be very effective for that. Yet, as language extensions beyond (decidable) DLs are being discussed, more general first-order logic systems are required, too. In this paper, we pursue this direction and consider automated reasoning on full first-order logic knowledge bases. We put forward an optimized approach of transforming such knowledge bases to clause logic. The transformations include a Brand-like transformation to eliminate equality, and a transformation that incorporates a blocking technique to "checks loops" in derivations. The latter transformation lets theorem provers terminate more often on satisfiable input formulas. It thus enables more robust automated reasoning support on ontologies, where disproving is a common task. While the transformations are applicable to any clause set, we concentrate in this paper on demonstrating their effectiveness on a standard test suite devised by the Semantic Web community.
A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity
A practically useful mathematical assistant system requires the sophisticated combination of interaction and automation. Central in such a system is the proof data structure, which has to maintain the current proof state and which has to allow the flexible interplay of various components including the human user. We describe a parameterized proof data structure for the management of proofs, which includes our experience with the development of two proof assistants. It supports and bridges the gap between abstract level proof explanation and low-level proof verification. The proof data structure enables, in particular, the flexible handling of lemmas, the maintenance of different proof alternatives, and the representation of different granularities of proof attempts.
Semantic Markup with TeX/LaTeX --- Towards an Integration of Deduction into the Publication Workflow
Working mathematicicans do not use deduction systems! This is a major stunbling block for the uptake of deduction systems as a mainstream technology. One of the reasons ist that currently most mathematical Knowledge and Publications are locked up in LaTeX documents, a format that is unsuitable for interfacing with theorem proving technologies as it is presentation-based.
We analyze the current practice of semi-semantic markup in LaTeX documents and supply a definition mechanism for semantic macros and a non-standard scoping construct for them, which is oriented at the semantic depency relation rather than the document structure. Concretely, we present a collection of TeX macro packages that allow to markup LaTeX documents semantically without leaving the document format, essentially turning LaTeX into a document format for mathematical knowledge management (MKM).
On this basis, it will be much simpler to include deduction technologies into the mathematics workflow and circumvent the practical barriers to deduction technology uptake in mathematics.
Organisation:
Christoph Wernhard <wernhard@uni-koblenz.de>