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.
Contents
INTRODUCTION
1.1 THE METHOD
1.2 READING INSTRUCTIONS
2 FIRST-ORDER LOGIC
2.1 WHAT IS LOGIC?
2.2 SYNTAX
2.3 PROOF SYSTEMS
2.4 INFERENCE
2.5 SEMANTICS
2.6 REFUTATION
3 FURTHER FIRST-ORDER FEATURES
3.1 UNIFICATION
3.2 PRENEX FORM
3.3 SKOLEMIZATION
3.4 CLAUSES
4 FIRST-ORDER PROOF PROCEDURES
4.1 RESOLUTION
4.2 TABLEAUX
4.3 DIFFERENCES AND SIMILARITIES
4.4 MORE EFFICIENT VERSIONS
4.5 SOUNDNESS AND COMPLETENESS
4.6 THE HISTORY OF PROLOG
5 EVALUATION
5.1 EFFICIENCY
5.2 EASE OF IMPLEMENTATION
5.3 IMPLEMENTATION – SIZE AND EFFORT
6 CONCLUSION
7 FUTURE WORK
APPENDIX
REFERENCES
Author: Andreas Folkler
Source: Blekinge Institute of Technology
Reference URL 1: Visit Now