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 -