Subsumption demodulation in first-order theorem proving

Abstract

in der modernen Gesellschaft. Die formale Software-Verifikation versucht, basierend auf logischem Schließen, verschiedene Anforderungen an die Korrektheit von Software mathematisch zu beweisen. Da jedoch das manuelle Beweisen solcher Aussagen mühsam und fehleranfällig ist, ist es erforderlich diese Aufgabe zu automatisieren, beispielsweise durch die Verwendung von automatischen Beweisern. Moderne automatische Beweiser für Logik erster Stufe mit Gleichheit sind bereits leistungsstarke Werkzeuge des automatischen Schließens. Allerdings stoßen die verfügbaren Systeme bei Problemen, die aus der Software-Verifikation kommen, noch häufig an ihre Grenzen. Insbesondere kann eine große Anzahl von bedingten Gleichungen Schwierigkeiten bereiten. Zur Verbesserung dieser Situation präsentieren wir in der vorliegenden Diplomarbeit eine neue Inferenzregel namens Subsumption Demodulation für Logik erster Stufe. Die grundlegende Idee von Subsumption Demodulation besteht darin, bedingte Gleichungen heranzuziehen um Terme in Klauseln, die die Bedingungen der Gleichung erfüllen, zu vereinfachen. Wir implementieren und evaluieren Forward Subsumption Demodulation mit Hilfe des auf dem Superpositionskalkül basierenden automatischen Beweisers Vampire. Erste Ergebnisse zeigen, dass Beweiser für Logik erster Stufe mit Forward Subsumption Demodulation neue Probleme lösen können, die bisher nicht von existierenden automatischen Beweisern gelöst werden konnten.

Ensuring correctness of software is becoming increasingly important in modern society, but still poses a difficult challenge. Reasoning-based software verification addresses this challenge by proving various requirements on software correctness. Performing such proofs manually is however tedious and error-prone, calling for the need to automate software correctness proofs, for example by using automated theorem provers. State-of-the-art first-order theorem provers for first-order logic with equality are powerful automated reasoning tools. However, there are still limitations concerning problem encodings that arise from software verification. In particular, a large number of conditional equalities can be problematic. In order to improve the situation, in this thesis we introduce a new inference rule in first-order theorem proving, called subsumption demodulation. The idea of subsumption demodulation is to use conditional equalities to simplify terms in clauses where the conditions are satisfied. We implement and evaluate forward subsumption demodulation using the superposition-based theorem prover Vampire. Our initial results show that forward subsumption demodulation in first-order theorem proving can solve many new problems that could so far not be solved by existing automated reasoners.