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.

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.