The Efficiency of Theorem Proving Strategies A Comparative and Asymp
- PDF / 15,398,275 Bytes
- 176 Pages / 419.528 x 595.276 pts Page_size
- 79 Downloads / 212 Views
The Efficiency of Theorem Proving Strategies
Computational Intelligence edited by Wolfgang Bibel, Walther von Hahn and Rudolf Kruse The books in this series contribute to the long-range goal of understanding and realizing intelligent behaviour in some environment. Thus they cover topics from the disciplines of Artificial Intelligence and Cognitive Science, combined also called Intellectics, as well as from fields interdisciplinarily related with these. Computational Intelligence comprises basic knowledge as well as applications.
Das Rechnende Gehirn
by Patricia S. Churchland and Terrence 1. Sejnowski
Neuronale Netze und Fuzzy-Systeme
by Detlef Nauck, Frank Klawonn and Rudolf Kruse
Fuzzy-Clusteranalyse
by Frank H6ppner, Frank Klawonn and Rudolf Kruse
Einfiihrung in Evolutionare Algorithmen by Volker Nissen
Neuronale Netze Grundlagen und Anwendungen by Andreas Scherer
The Efficiency of Theorem Proving Strategies by David A. Plaisted and Yunshan Zhu
Among others the following books were published in the series of Artificial Intelligence
Automated Theorem Proving by Wolfgang Bibel (out of print)
Fuzzy Sets and Fuzzy Logic Foundation of Application - from a Mathematical Point of View by Siegfried Gottwald
Fuzzy Systems in Computer Science edited by Rudolf Kruse, J6rg Gebhard and Rainer Palm
David A. Plaisted Yunshan Zhu
The Efficiency
of Theorem Proving Strategies
A Comparative and Asymptotic Analysis
II Vlewag
All righ ts reserved © Friedr. Vieweg & Sohn Verlagsgesellschaft mbH, Braunschweig/Wiesbaden, 1997
Vieweg is a subsidiary company of the Bertelsmann Professional Information.
No part of this pUblication may be reproduced, stored in a retrieval system or transmitted, mechanical, photocopying or otherwise, without prior permission of the copyright holder.
http://www.vieweg.de Produced by Rosch-Buch, ScheBlitz Printed on acid-free paper
ISSN 0949-5665 ISBN 978-3-322-93862-6 (eBook) ISBN 978-3-528-05574-5 DOI 10.1007/978-3-322-93862-6
Contents 1 The Propositional Complexity of First-Order Theorem Proving Strategies 1.1 Introduction...... . . . . . . . . . . . . . . . 1.2 First Order Logic and Refutational Theorem Proving .. . . . . . . . . 1.3 Search Space Formalism ....... 1.4 Measures of Search Duplication 1.5 Analysis of Duplication for Various Strategies 1.5.1 Hard sets of clauses for the strategies 1.5.2 Hyper-resolution 1.5.3 Pl deduction ......... 1.5.4 A-ordering............ 1.5.5 Implications for term rewriting 1.5.6 Proof dags . . . . . . . . . . . . 1.5.7 Other properties of clause sets . 1.5.8 All-negative resolution .... 1.5.9 All-negative resolution with ordering 1.5.10 A-ordering and proof dags 1.5.11 SLD-resolution .. 1.5.12 Set of support. . . 1.5.13 Model elimination. 1.5.14 Lemmas and caching 1.5.15 The MESON strategy 1.5.16 Problem reduction formats. 1.5.17 Clause linking . . . 1.5.18 Connection calculi 1.5.19 Caching . . . . . .
1 1 7 8 9 13 16 22 23 24 27 28 29 29 31 40 49 51 52 53 55 55 56 56 57
1.6 1. 7 1.8
Preventing Unit Simplifications Additional Hard Sets o
Data Loading...
