TY - JOUR A1 - Frank, Mario T1 - Axiom relevance decision engine : technical report N2 - This document presents an axiom selection technique for classic first order theorem proving based on the relevance of axioms for the proof of a conjecture. It is based on unifiability of predicates and does not need statistical information like symbol frequency. The scope of the technique is the reduction of the set of axioms and the increase of the amount of provable conjectures in a given time. Since the technique generates a subset of the axiom set, it can be used as a preprocessor for automated theorem proving. This technical report describes the conception, implementation and evaluation of ARDE. The selection method, which is based on a breadth-first graph search by unifiability of predicates, is a weakened form of the connection calculus and uses specialised variants or unifiability to speed up the selection. The implementation of the concept is evaluated with comparison to the results of the world championship of theorem provers of the year 2012 (CASC J6). It is shown that both the theorem prover leanCoP which uses the connection calculus and E which uses equality reasoning, can benefit from the selection approach. Also, the evaluation shows that the concept is applyable for theorem proving problems with thousands of formulae and that the selection is independent from the calculus used by the theorem prover. N2 - Dieser technische Report beschreibt die Konzeption, Implementierung und Evaluation eines Verfahrens zur Auswahl von logischen Formeln bezüglich derer Relevanz für den Beweis einer logischen Formel. Das Verfahren wird ausschließlich für die Prädikatenlogik erster Ordnung angewandt, wenngleich es auch für höherstufige Prädikatenlogiken geeignet ist. Das Verfahren nutzt eine unifikationsbasierte Breitensuche im Graphen wobei jeder Knoten im Graphen ein Prädikat und jede existierende Kante eine Unifizierbarkeitsrelation ist. Ziel des Verfahrens ist die Reduktion einer gegebenen Menge von Formeln auf eine für aktuelle Theorembeweiser handhabbare Größe. Daher ist das Verfahren als Präprozess-Schritt für das automatische Theorembeweisen geeignet. Zur Beschleunigung der Suche wird neben der Standard-Unifikation eine abgeschwächte Unifikation verwendet. Das System wurde während der Weltmeisterschaft der Theorembeweiser im Jahre 2014 (CASC J6) in Manchester zusammen mit dem Theorembeweiser leanCoP eingereicht und konnte leanCoP dabei unterstützen, Probleme zu lösen, die leanCoP alleine nicht handhaben kann. Die Tests mit leanCoP und dem Theorembeweiser E im Nachgang zu der Weltmeisterschaft zeigen, dass das Verfahren unabhängig von dem verwendeten Kalkül ist und bei beiden Theorembeweisern positive Auswirkungen auf die Beweisbarkeit von Problemen mit großen Formelmengen hat. KW - Relevanz KW - Graphensuche KW - Theorembeweisen KW - Preprocessing KW - Unifikation KW - relevance KW - graph-search KW - preprocessing KW - unification KW - theorem Y1 - 2012 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-72128 ER - TY - THES A1 - Frank, Mario T1 - TEMPLAR : efficient determination of relevant axioms in big formula sets for theorem proving N2 - This document presents a formula selection system for classical first order theorem proving based on the relevance of formulae for the proof of a conjecture. It is based on unifiability of predicates and is also able to use a linguistic approach for the selection. The scope of the technique is the reduction of the set of formulae and the increase of the amount of provable conjectures in a given time. Since the technique generates a subset of the formula set, it can be used as a preprocessor for automated theorem proving. The document contains the conception, implementation and evaluation of both selection concepts. While the one concept generates a search graph over the negation normal forms or Skolem normal forms of the given formulae, the linguistic concept analyses the formulae and determines frequencies of lexemes and uses a tf-idf weighting algorithm to determine the relevance of the formulae. Though the concept is built for first order logic, it is not limited to it. The concept can be used for higher order and modal logik, too, with minimal adoptions. The system was also evaluated at the world championship of automated theorem provers (CADE ATP Systems Competition, CASC-24) in combination with the leanCoP theorem prover and the evaluation of the results of the CASC and the benchmarks with the problems of the CASC of the year 2012 (CASC-J6) show that the concept of the system has positive impact to the performance of automated theorem provers. Also, the benchmarks with two different theorem provers which use different calculi have shown that the selection is independent from the calculus. Moreover, the concept of TEMPLAR has shown to be competitive to some extent with the concept of SinE and even helped one of the theorem provers to solve problems that were not (or slower) solved with SinE selection in the CASC. Finally, the evaluation implies that the combination of the unification based and linguistic selection yields more improved results though no optimisation was done for the problems. N2 - Dieses Dokument stellt ein System vor, das aus einer (großen) gegebenen Menge von Formeln der klassischen Prädikatenlogik eine Teilmenge auswählt, die für den Beweis einer logischen Formel relevant sind. Ziel des Systems ist, die Beweisbarkeit von Formeln in einer festen Zeitschranke zu ermöglichen oder die Beweissuche durch die eingeschränkte Formelmenge zu beschleunigen. Das Dokument beschreibt die Konzeption, Implementierung und Evaluation des Systems und geht dabei auf die zwei verschiedenen Ansätze zur Auswahl ein. Während das eine Konzept eine Graphensuche wahlweise auf den Negations-Normalformen oder Skolem-Normalformen der Formeln durchführt, indem Pfade von einer Formel zu einer anderen durch Unifikation von Prädikaten gebildet werden, analysiert das andere Konzept die Häufigkeiten von Lexemen und bildet einen Relevanzwert durch Anwendung des in der Computerlinguistik bekannten tf-idf-Maßes. Es werden die Ergebnisse der Weltmeisterschaft der automatischen Theorembeweiser (CADE ATP Systems Competition, CASC-24) vorgestellt und der Effekt des Systems für die Beweissuche analysiert. Weiterhin werden die Ergebnisse der Tests des Systems auf den Problemen der Weltmeisterschaft aus dem Jahre 2012 (CASC-J6) vorgestellt. Es wird darauf basierend evaluiert, inwieweit die Einschränkungen die Theorembeweiser bei dem Beweis komplexer Probleme unterstützen. Letztendlich wird gezeigt, dass das System einerseits positive Effekte für die Theorembeweiser hat und andererseits unabhängig von dem Kalkül ist, den die Theorembeweiser nutzen. Ferner ist der Ansatz unabhängig von der genutzten Logik und kann prinzipiell für alle Stufen der Prädikatenlogik und Aussagenlogik sowie Modallogik genutzt werden. Dieser Aspekt macht den Ansatz universell im automatischen Theorembeweisen nutzbar. Es zeigt sich, dass beide Ansätze zur Auswahl für verschiedene Formelmengen geeignet sind. Es wird auch gezeigt, dass die Kombination beider Ansätze eine signifikante Erhöhung der beweisbaren Formeln zur Folge hat und dass die Auswahl durch die Ansätze mit den Fähigkeiten eines anderen Auswahl-Systems mithalten kann. KW - Theorembeweisen KW - Relevanz KW - Selektion KW - Liguistisch KW - Unifikation KW - relevance KW - selection KW - proving KW - linguistic KW - theorem Y1 - 2013 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-72112 ER - TY - THES A1 - Frank, Mario T1 - On synthesising Linux kernel module components from Coq formalisations T1 - Über die Synthese von Linux Kernel- Modul-Komponenten aus Coq-Formalisierungen N2 - This thesis presents an attempt to use source code synthesised from Coq formalisations of device drivers for existing (micro)kernel operating systems, with a particular focus on the Linux Kernel. In the first part, the technical background and related work are described. The focus is here on the possible approaches to synthesising certified software with Coq, namely the extraction to functional languages using the Coq extraction plugin and the extraction to Clight code using the CertiCoq plugin. It is noted that the implementation of CertiCoq is verified, whereas this is not the case for the Coq extraction plugin. Consequently, there is a correctness guarantee for the generated Clight code which does not hold for the code being generated by the Coq extraction plugin. Furthermore, the differences between user space and kernel space software are discussed in relation to Linux device drivers. It is elaborated that it is not possible to generate working Linux kernel module components using the Coq extraction plugin without significant modifications. In contrast, it is possible to produce working user space drivers both with the Coq extraction plugin and CertiCoq. The subsequent parts describe the main contributions of the thesis. In the second part, it is demonstrated how to extend the Coq extraction plugin to synthesise foreign function calls between the functional language OCaml and the imperative language C. This approach has the potential to improve the type-safety of user space drivers. Furthermore, it is shown that the code being synthesised by CertiCoq cannot be used in kernel space without modifications to the necessary runtime. Consequently, the necessary modifications to the runtimes of CertiCoq and VeriFFI are introduced, resulting in the runtimes becoming compatible components of a Linux kernel module. Furthermore, justifications for the transformations are provided and possible further extensions to both plugins and solutions to failing garbage collection calls in kernel space are discussed. The third part presents a proof of concept device driver for the Linux Kernel. To achieve this, the event handler of the original PC Speaker driver is partially formalised in Coq. Furthermore, some relevant formal properties of the formalised functionality are discussed. Subsequently, a kernel module is defined, utilising the modified variants of CertiCoq and VeriFFI to compile a working device driver. It is furthermore shown that it is possible to compile the synthesised code with CompCert, thereby extending the guarantee of correctness to the assembly layer. This is followed by a performance evaluation that compares a naive formalisation of the PC speaker functionality with the original PC Speaker driver pointing out the weaknesses in the formalisation and possible improvements. The part closes with a summary of the results, their implications and open questions being raised. The last part lists all used sources, separated into scientific literature, documentations or reference manuals and artifacts, i.e. source code. N2 - Die vorliegende Dissertation präsentiert einen Ansatz zur Nutzung von Quellcode, der aus der Coq-Formalisierung eines Gerätetreibers generiert wurde, für bestehende (Mikrokernel-)Betriebssysteme, im Speziellen den Linux-Kernel. Im ersten Teil erfolgt eine Beschreibung der relevanten technischen Aspekte sowie des aktuellen Forschungsstandes. Dabei liegt der Fokus auf der Synthese von funktionalem Code durch das Coq Extraction Plugin und von Clight Code durch das CertiCoq Plugin. Des Weiteren wird dargelegt, dass die Implementierung von CertiCoq im Gegensatz zu der des Coq Extraction Plugin verifiziert ist, wodurch sich eine Korrektheitsgarantie für den generierten Clight Code ableiten lässt. Darüber hinaus werden die Unterschiede zwischen User Space und Kernel Space Software in Bezug auf Linux-Treiber erörtert. Unter Berücksichtigung der technischen Einschränkungen wird dargelegt, dass der durch das Coq Extraction Plugin generierte Code ohne gravierende Anpassungen der Laufzeitumgebung nicht als Teil eines Kernel Space Treibers nutzbar ist. Die nachfolgenden Teile der Dissertation behandeln den Beitrag dieser Arbeit. Im zweiten Teil wird dargelegt, wie das Coq Extraction Plugin derart erweitert werden kann, dass typsichere Aufrufe zwischen den Sprachen OCaml und C generiert werden können. Dies verhindert spezifische Kompilationsfehler aufgrund von Typfehlern. Des Weiteren wird aufgezeigt, dass der durch CertiCoq generierte Code ebenfalls nicht im Kernel Space genutzt werden kann, da die Laufzeitumgebung technische Einschränkungen verletzt. Daher werden die notwendigen Anpassungen an der vergleichsweise kleinen Laufzeitumgebung sowie an VeriFFI vorgestellt und deren Korrektheit begründet. Anschließend werden mögliche Erweiterungen beider Plugins sowie die Möglichkeit der Behandlung von fehlschlagenden Aufrufen der Garbage Collection von CertiCoq im Kernel Space erörtert. Im dritten Teil wird als Machbarkeitsstudie im ersten Schritt der Event-Handler des Linux PC Speaker Treibers beschrieben und eine naive Coq-Formalisierung sowie wichtige formale Eigenschaften dargelegt. Dann wird beschrieben, wie ein Kernel-Modul und dessen Kompilation definiert werden muss, um einen lauffähigen Linux Kernel Treiber zu erhalten. Des Weiteren wird erläutert, wie die generierten Teile dieses Treibers mit dem verifizierten Kompiler CompCert übersetzt werden können, wodurch auch eine Korrektheit für den resultierenden Assembler-Code gilt. Im Anschluss erfolgt eine Evaluierung der Performance des aus der naiven Coq-Formalisierung generierten Codes im Vergleich zum originalen PC-Speaker Treiber. Dabei werden die Schwächen der Formalisierung sowie mögliche Verbesserungen diskutiert. Der Teil wird mit einer Zusammenfassung der Ergebnisse sowie der daraus resultierenden offenen Fragen abgeschlossen. Der letzte Teil gibt eine Übersicht über genutzte Quellen und Hilfsmittel, unterteilt in wissenschaftliche Literatur, Dokumentationen sowie Software-Artefakte. KW - Linux device drivers KW - Coq KW - CertiCoq KW - synthesis KW - compilation KW - Geräte-Treiber KW - Linux KW - Coq KW - CertiCoq KW - Synthese KW - Kompilation Y1 - 2024 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-642558 ER -