Automated Model Building

Front Cover
Springer Science & Business Media, Sep 13, 2004 - Philosophy - 341 pages
0 Reviews
On the history of the book: In the early 1990s several new methods and perspectives in au- mated deduction emerged. We just mention the superposition calculus, meta-term inference and schematization, deductive decision procedures, and automated model building. It was this last ?eld which brought the authors of this book together. In 1994 they met at the Conference on Automated Deduction (CADE-12) in Nancy and agreed upon the general point of view, that semantics and, in particular, construction of models should play a central role in the ?eld of automated deduction. In the following years the deduction groups of the laboratory LEIBNIZ at IMAG Grenoble and the University of Technology in Vienna organized several bilateral projects promoting this topic. This book emerged as a main result of this cooperation. The authors are aware of the fact, that the book does not cover all relevant methods of automated model building (also called model construction or model generation); instead the book focuses on deduction-based symbolic methods for the construction of Herbrand models developed in the last 12 years. Other methods of automated model building, in particular also ?nite model building, are mainly treated in the ?nal chapter; this chapter is less formal and detailed but gives a broader view on the topic and a comparison of di?erent approaches. Howtoreadthisbook: In the introduction we give an overview of automated deduction in a historical context, taking into account its relationship with the human views on formal and informal proofs.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

III
1
IV
4
V
7
VI
9
VII
19
IX
24
X
29
XI
33
XLIII
219
XLIV
220
XLV
224
XLVI
230
XLVII
231
XLVIII
233
XLIX
236
L
247

XII
35
XIII
39
XIV
43
XV
45
XVI
55
XVII
74
XVIII
93
XIX
99
XX
119
XXI
133
XXII
151
XXIII
152
XXIV
154
XXV
159
XXVI
161
XXVII
163
XXVIII
175
XXIX
176
XXX
179
XXXII
180
XXXIII
185
XXXV
189
XXXVII
194
XXXVIII
200
XXXIX
201
XL
204
XLI
213
XLII
218
LI
248
LII
251
LIII
255
LVI
256
LVII
260
LVIII
273
LIX
274
LX
277
LXI
279
LXII
284
LXIII
290
LXIV
292
LXV
294
LXVI
296
LXVII
297
LXVIII
299
LXX
304
LXXI
307
LXXII
308
LXXIII
309
LXXV
310
LXXVI
311
LXXVII
319
LXXVIII
321
LXXIX
323
LXXX
327
Copyright

Other editions - View all

Common terms and phrases

Popular passages

Page 335 - M. Rusinowitch, Proving Refutational Completeness of Theorem Proving Strategies: the Transfinite Semantic Tree Method, Journal of the ACM, 38, pp.
Page 327 - Read ings in Artificial Intelligence, pages 334-348. Tioga, Ca. Gaschnig, J. (1982). Application of the Prospector system to geological exploration problems. In Hayes, JE, Michie, D., and Pao, Y.-H., editors, Machine Intelligence 10 pages 301-323. Horwood, Chichester. Klein, M. and Lu, SC-Y. (1989). Conflict resolution in co-operative design. AI in En gineering, 4(4):168-180.
Page 332 - De Bruijn, NG (1980) A survey of the project Automath. In: Seldin & Hindley (eds.) To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalisms. Academic Press. 579-606. Bunt, HC (1989) Information dialogues as communicative action in relation to partner modeling and information processing. In: Taylor, MM, Neel, F. & Bouwhuis, DG (eds.) The Structure...

Bibliographic information