Tableaux Versus Resolution a Comparison

Article type: Research Article

Authors: Ophelders, W.M.J. | De Swart, H.C.M.

Affiliations: Department of Philosophy, Tilburg University, P.O. Box 90153, 5000 LE Tilburg, The Netherlands

Abstract: In [13] we have presented the ideas underlying an automated theorem prover based on tableaux extended with unification under restrictions. In [6] a full description of an implementation of this theorem prover in PROLOG is given. In this paper we first shortly repeat the main ideas, referring to [13] for more details. Next we present the test results of our theorem prover mainly with respect to Pelletier’s 75 problems for testing automatic theorem provers ([7]). We also give a comparison of our results with the results obtained by the resolution-based theorem provers PCPROVE and OTTER and by the tableau-based theorem provers of M. Fitting and S. Reeves. Short discussions of these theorem provers accompany the test results. For more elaborate discussions the reader is referred to [6].

DOI: 10.3233/FI-1993-182-403

Journal: Fundamenta Informaticae, vol. 18, no. 2-4, pp. 109-127, 1993