The Search Efficiency of Theorem Proving Strategies

Plaisted, David A.

doi:10.1007/3-540-58156-1_5

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

The Search Efficiency of Theorem Proving Strategies

MPS-Authors

Plaisted, David A.
Max Planck Society;

External Resource

https://rdcu.be/dtohi
(Publisher version)

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

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: https://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.