Inlämning av Examensarbete / Submission of Thesis

Andreas Folkler MSE-2002:4, pp. 40. Inst. för programvaruteknik och datavetenskap/Dept. of Software Engineering and Computer Science, 2002.

The work

Författare / Author: Andreas Folkler
andreas@folkler.net
Titel / Title: Automated Theorem Proving - Resolution vs. Tableaux
Översatt titel / Translated title: Automatisk Teorembevisning - Resolution vs Tablå
Abstrakt Abstract:

The purpose of this master thesis was to investigate which of the two methods, resolution and tableaux, that is the most appropriate for automated theorem proving. This was done by implementing an automated theorem prover, comparing and documenting implementation problems, and measuring proving efficiency.
In this thesis, I conclude that the resolution method might be more suitable for an automated theorem prover than tableaux, in the aspect of ease of implementation. Regarding the efficiency, the test results indicate that resolution is the better choice.

Populärvetenskaplig beskrivning / Popular science summary: Syftet med detta magisterarbete var att undersöka vilken av de två metoderna, resolution och tablå, som är mest lämpad för automatisk teorembevisning. Detta gjordes genom att implementera en automatisk teorembevisare, jämföra och dokumentera problem, samt att mäta prestanda för bevisning.
I detta arbete drar jag slutsatsen att resolutionsmetoden förmodligen är mer lämpad än tablåmetoden för en automatisk teorembevisare, med avseende på hur svår den är att implementera. När det gäller prestanda indikerar utförda tester att resolutionsmetoden är det bästa valet.
Ämnesord / Subject: Datavetenskap - Computer Science\Software Engineering
Datavetenskap - Computer Science\Artificial Intelligence
Datavetenskap - Computer Science\General
Nyckelord / Keywords: First-order logic, tableaux, resolution, efficiency, ease of implementation

Publication info

Dokument id / Document id:
Program:/ Programme Programvaruteknik/Software Engineering
Registreringsdatum / Date of registration: 09/16/2004
Uppsatstyp / Type of thesis: D-Uppsats/Magister/Master

Context

Handledare / Supervisor: Bertil Ekdahl
bertil.ekdahl@cs.lth.se
Examinator / Examiner: Claes Wohlin
Organisation / Organisation: Blekinge Institute of Technology
Institution / School: Inst. för programvaruteknik och datavetenskap/Dept. of Software Engineering and Computer Science
Inst. för Programvaruteknik och Datavetenskap S-372 25 Ronneby
+46 455 780 00
http://www.ipd.bth.se/

Files & Access

Bifogad uppsats fil(er) / Files attached: masterthesis100.pdf (410 kB, öppnas i nytt fönster)