Title: Reasoning in first-order theories with extensionality
Language: English
Authors: Kragl, Bernhard 
Qualification level: Diploma
Advisor: Kovacs, Laura 
Issue Date: 2014
Citation: 
Kragl, B. (2014). Reasoning in first-order theories with extensionality [Diploma Thesis]. reposiTUm. https://doi.org/10.34726/hss.2014.23884
Number of Pages: 44
Qualification level: Diploma
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.
Keywords: Automated reasoning; first-order theorem proving; formal methods; program verification
URI: https://doi.org/10.34726/hss.2014.23884
http://hdl.handle.net/20.500.12708/7495
DOI: 10.34726/hss.2014.23884
Library ID: AC11703178
Organisation: E185 - Institut für Computersprachen 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:



Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.

Page view(s)

35
checked on May 7, 2022

Download(s)

83
checked on May 7, 2022

Google ScholarTM

Check