Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
  Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben
Konferenzbeitrag

The Search Efficiency of Theorem Proving Strategies

MPG-Autoren

Plaisted,  David A.
Max Planck Society;

Externe Ressourcen

https://rdcu.be/dtohi
(Verlagsversion)

Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-0014-ADB2-B
Zusammenfassung
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.