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.

Zenon AB is an it-company of which, this thesis was made in collaboration with. Zenon AB has clients that generate large amounts of data, therefore it is important for Zenon AB that they make competent choices of database management systems (DBMS) when designing systems for their clients. This thesis will therefore entail research carried out into the comparison of DBMS. Nowadays, there exists a large variety of DBMS. Despite this, there seems to be a lack of comparisons between types of DBMS and therefore a lack clarity of when each type should be used. Thus, this thesis aims to highlight these differences of DBMS types by creating a tailored test for each DBMS type and compare how each type performs in each-others area of specialization. This process will show how big the differences can be and highlight the importance of the choice of DBMS. The time it takes, and how simple DBMSs are to implement seems to be a factor most developers take into consideration when choosing DBMS but there is little research on how to compare the aspect. Therefore, this thesis will investigate the viability of a method to compare how easy the DBMSs are to implement into systems by querying programming help forums such as Stackoverflow. / <p>Examensarbetet är utfört vid Institutionen för teknik och naturvetenskap (ITN) vid Tekniska fakulteten, Linköpings universitet</p>