Reasoning in first-order theories with extensionality

Abstract

Extensionalitätsaxiome sind zentral für das Schließen über Containerobjekte, wie etwa Mengen in der Mathematik, oder Arrays und Funktionen in der Programmanalyse. Ein Extensionalitätsaxiom besagt, dass zwei Container genau dann gleich sind, wenn sie dieselben Elemente (an denselben Indizes) beinhalten. Die Anwendung eines Extensionalitätsaxioms ist oft erforderlich um zu zeigen, dass zwei Container gleich sind - ein typisches Beispiel ist das Mengenlehrentheorem (-x)(-y) x - y = y - x. Obwohl das Beweisen solcher Mengenidentitäten mittels Extensionalität für Menschen kein Problem darstellt, sind diese für automatische Beweiser aufgrund der verwendeten Kalküle problematisch. In dieser Diplomarbeit zeigen wir, wie das Hinzufügen einer neuen Inferenzregel, genannt Extensionalitätsresolution, automatischen Beweisern erlaubt, mühelos Probleme zu lösen, welche kein moderner automatischer Beweiser erster Stufe lösen kann. Wir veranschaulichen dies anhand von zahlreichen Problemen über Mengen und Arrays durch Erweiterung des weltweit führenden automatischen Beweisers VAMPIRE um Extensionalitätsresolution.

Extensionality axioms are common when reasoning about collections, such as sets in mathematics, or arrays and functions in program analysis. An extensionality axiom asserts that two collections are equal if they consist of the same elements (at the same indices). Using extensionality is often required to show that two collections are equal, a typical example is the set theory theorem (-x)(-y) x - y = y - x. Interestingly, while humans have no problem with proving such set identities using extensionality, they are very hard for superposition theorem provers because of the calculi they use. In this thesis we show how addition of a new inference rule, called extensionality resolution, allows first-order theorem provers easily solve problems no modern first-order theorem prover can solve. We illustrate this by running the world-leading theorem prover VAMPIRE with extensionality resolution on a number of set theory and array problems.