Extending the E-Hyper Tableau Calculus for Reasoning with the Unique Name Assumption
- In automated theorem proving, there are some problems that need information on the inequality of certain constants. In most cases this information is provided by adding facts which explicitly state that two constants are unequal. Depending on the number of constants, a huge amount of this facts can clutter the knowledge base and distract the author and readers of the problem from its actual proposition. For most cases it is save to assume that a larger knowledge base reduces the performance of a theorem prover, which is another drawback of explicit inequality facts. Using the unique name assumption in those reasoning tasks renders the introduction of inequality facts obsolete as the unique name assumptions states that two constants are identical iff their interpretation is identical. Implicit handling of non-identical constants makes the problems easier to comprehend and reduces the execution time of reasoning. In this thesis we will show how to integrate the unique name assumption into the E-hyper tableau calculus and that the modified calculus is sound and complete. The calculus will be implemented into the E-KRHyper theorem prover and we will show, by empiric evaluation, that the changed implementation, which is able to use the unique name assumption, is superior to the traditional version of E-KRHyper.
- In einigen Bereichen des automatischen Theorembeweisens benötigt man das Wissen, dass Konstanten paarweise ungleich sind. Um dieses zu erreichen, fügt man Fakten, die dieses Wissen explizit angeben, zu den Wissensbasen hinzu. Wenn man diese Eigenschaft für viele Konstanten definieren muss, wird die Klauselmenge der Wissensbasen schnell sehr umfangreich und wegen der vielen - eigentlich irrelevanten - Ungleichheiten kann man den Blick auf das eigentlich formalisierte Problem verlieren. Da die Größe der Wissensbasis in vielen Fällen Einfluss auf die Geschwindigkeit hat, ist es auch aus diesem Grund sinnvoll, die Anzahl dieser Fakten gering zu halten. Die unique name assumption erlaubt auf die Einführung der Ungleichheits-Fakten zu verzichten, da sie festlegt, dass zwei Konstanten genau dann gleich sind, wenn ihre Interpretationen identisch sind. Auf diesem Wege lässt sich das Aufblähen von Wissensbasen mit Ungleichheits-Fakten verhinde. In dieser Arbeit wird der E-Hyper-Tableau-Kalkül erweitert um die unique name assumption nutzen zu können. Der in dieser Arbeit entwickelte Kalkül ist vollständig und korrekt, was durch formale Beweise in dieser Arbeit belegt wird. Um zu zeigen, dass die native Behandlung von Ungleichheiten dem Einführen von Ungleichheits-Fakten überlegen ist, wird der Kalkül in den Theorembeweiser E-KRHyper implementieren. Der Theorembeweiser E-KRHyper ist ein etabliertes System und basiert in seiner ursprünglichen Version auf dem E-Hyper-Tableau. Mit systematischen Tests wird dann gezeigt, dass die entwickelte Implementierung des erweiterten Kalküls nie schlechter ist, als der original E-KRHyper, diesen aber in einigen Fällen in der Ausführungsgeschwindigkeit deutlich übertrifft.
Author: | Markus Bender |
---|---|
URN: | urn:nbn:de:kola-5991 |
Advisor: | Ulrich Furbach |
Document Type: | Diploma Thesis |
Language: | English |
Date of completion: | 2012/01/30 |
Date of publication: | 2012/01/30 |
Publishing institution: | Universität Koblenz-Landau, Campus Koblenz, Universitätsbibliothek |
Granting institution: | Universität Koblenz, Fachbereich 4 |
Release Date: | 2012/01/30 |
Tag: | E-Hyper Tableau; E-KRHyper; distinct object identifiers; unique name assumption |
GND Keyword: | Automatisches Beweisverfahren; Logik; Schlussfolgern |
Number of pages: | viii, 70 Seiten |
Institutes: | Fachbereich 4 / Fachbereich 4 |
Dewey Decimal Classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Licence (German): | Es gilt das deutsche Urheberrecht: § 53 UrhG |