The Efficiency of Theorem Proving Strategies

Bok av David A. Plaisted och Yunshan Zhu
Dieses Buch in englischer Sprache widmet sich dem Thema der Effizienz von Beweisstrategien und bietet eine vergleichende und asymptotische Analyse. Das Werk stellt erstmalig asymptotische Schranken fur die Grosse der von vielen gebrauchlichen Beweisstrategien erzeugten Suchfelder bereit. Auf diese Weise erlaubt es ein theoretisches Verstandnis der Effizienz unterschiedlicher Beweisverfahren. Es wird ein fundamental neues Werkzeug fur den Effizienzvergleich von Beweisstrategien bereitgestellt. Die zweite Auflage wurde gegenuber der ersten leicht verbessert, neuere Literaturhinweise zudem berucksichtigt. This book is unique in that it gives asymptotic bounds on the sizes of the search spaces generated by many common theorem proving strategies. Thus it permits one to gain a theoretical unterstanding of the efficiencies of many different theorem proving methods. This is a fundamental new tool in the comparative study of theorem proving strategies.