Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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
Identifiers
URN: urn:nbn:se:bth-5531Local ID: oai:bth.se:arkivex0599250D08DF003DC1256B94006EFA6AOAI: oai:DiVA.org:bth-5531DiVA: diva2:832916
Uppsok
Technology
Supervisors
Available from: 2015-04-22 Created: 2002-04-07 Last updated: 2015-06-30Bibliographically approved

Open Access in DiVA

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

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

Search outside of DiVA

GoogleGoogle Scholar
Total: 258 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: 74 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf