This Article 
 Bibliographic References 
 Add to: 
Experimental Results on Subgoal Reordering
June 1990 (vol. 39 no. 6)
pp. 845-848

The effect on the performance of a goal-oriented theorem power is studied on subgoal re-ordering using some simple synthetic heuristics. It is shown that subgoal reordering using these simple heuristics has a considerable impact on the performance of the prover on a large set of test problems. Some heuristics even provide equally good, and often better, performance as to the hand ordering of the input clauses. The merit of the approach seems to be that the syntactic aspect of theorem proving is considered. This approach is simple in form and cheap in its evaluation, and often provides good heuristics.

[1] C. L. Chang and R. C. T. Lee,Symbolic Logic and Mechanical Theorem Proving. New York: Academic, 1973.
[2] H. Gelernter, "Realization of a geometry theorem-proving machine," inProc. ICIP, Paris UNESCO House, 1959, pp. 273-282.
[3] M.R. Genesereth and N.J. Nilsson,Logical Foundations of Artificial Intelligence, Morgan Kaufmann, San Mateo, Calif., 1987.
[4] R. E. Korf, "Depth-first iterative deepening: An optimal admissible tree search,"Artificial Intell., vol. 25, pp. 97-109, 1985.
[5] R. Kowalski and D. Kuehner, "Linear resolution with selection function,"Artif. Intell., vol. 2, pp. 227-260, 1971.
[6] D. A. Plaisted, "Non-Horn clause logic programming without contrapositives,"J. Automat. Reasoning, vol. 4, no. 3, Sept. 1988.
[7] R. Reiter, "A semantically guided deductive system for automatic theorem proving,"IEEE Trans. Comput., vol. C-25, no. 4, pp. 328-334, Apr. 1976.
[8] D. E. Smith and M. R. Genesereth, "Ordering conjunctive queries,"Artificial Intell., vol. 26, pp. 171-215, 1985.
[9] M. E. Stickel, "A PROLOG technology theorem prover: Implementation by an extended PROLOG compiler," inProc. IJCAI, Oxford, England, July 1986, pp. 573-587.
[10] T. C. Wang and W. W. Bledsoe, "Hierarchical deduction,"J. Automat. Reasoning, vol. 3, no. 1, 1987.

Index Terms:
subgoal reordering; goal-oriented theorem power; synthetic heuristics; hand ordering; syntactic aspect; theorem proving.
X. Nie, D.A. Plaisted, "Experimental Results on Subgoal Reordering," IEEE Transactions on Computers, vol. 39, no. 6, pp. 845-848, June 1990, doi:10.1109/12.53609
Usage of this product signifies your acceptance of the Terms of Use.