de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

The Search Efficiency of Theorem Proving Strategies

MPS-Authors

Plaisted,  David A.
Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

Plaisted, D. A. (1994). The Search Efficiency of Theorem Proving Strategies. In A. Bundy (Ed.), Proceedings of the 12th International Conference on Automated Deduction (CADE-12) (pp. 57-71). Berlin, Germany: Springer.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-ADB2-B
Abstract
We analyze the search efficiency of a number of common refutational theorem proving strategies for first-order logic. We show that most of them produce search spaces of exponential size even on simple sets of clauses, or else are not sensitive to the goal. We also discuss clause linking, a new procedure that uses a reduction to propositional calculus, and show that it, together with methods that cache subgoals, have behavior that is more favorable in some respects.