Experimental results on subgoal reordering

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

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on computers 1990-06, Vol.39 (6), p.845-848
Main Authors: Nie, X., Plaisted, D.A.
Format: Article
Language:English
Subjects:
Applied sciences
Artificial intelligence
Computer science
control theory
systems
Exact sciences and technology
Terminology
Testing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.< >
ISSN:0018-9340
1557-9956
DOI:10.1109/12.53609