Change search
ReferencesLink to record
Permanent link

Direct link
Automated Theorem Proving: Resolution vs. Tableaux
Blekinge Institute of Technology, Department of Software Engineering and Computer Science.
2002 (English)Independent thesis Advanced level (degree of Master (One Year))Student thesisAlternative title
Automatisk Teorembevisning : Resolution vs Tablå (Swedish)
Abstract [en]

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.

Abstract [sv]

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.

Place, publisher, year, edition, pages
2002. , 40 p.
Keyword [en]
First-order logic, tableaux, resolution, efficiency, ease of implementation
National Category
Computer Science Software Engineering
URN: urn:nbn:se:bth-5531Local ID: diva2:832916
Available from: 2015-04-22 Created: 2002-04-07 Last updated: 2015-06-30Bibliographically approved

Open Access in DiVA

fulltext(400 kB)133 downloads
File information
File name FULLTEXT01.pdfFile size 400 kBChecksum SHA-512
Type fulltextMimetype application/pdf

By organisation
Department of Software Engineering and Computer Science
Computer ScienceSoftware Engineering

Search outside of DiVA

GoogleGoogle Scholar
Total: 133 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 31 hits
ReferencesLink to record
Permanent link

Direct link