Automated Theorem Proving : Resolution vs. Tableaux

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 effi...

Full description

Bibliographic Details
Main Author: Folkler, Andreas
Format: Others
Language:English
Published: Blekinge Tekniska Högskola, Institutionen för programvaruteknik och datavetenskap 2002
Subjects:
Online Access:http://urn.kb.se/resolve?urn=urn:nbn:se:bth-5531