Dynamic Logic

Przednia okładka
MIT Press, 29 wrz 2000 - 476
1 recenzji

This book provides the first comprehensive introduction to Dynamic Logic.

Among the many approaches to formal reasoning about programs, Dynamic Logic enjoys the singular advantage of being strongly related to classical logic. Its variants constitute natural generalizations and extensions of classical formalisms. For example, Propositional Dynamic Logic (PDL) can be described as a blend of three complementary classical ingredients: propositional calculus, modal logic, and the algebra of regular events. In First-Order Dynamic Logic (DL), the propositional calculus is replaced by classical first-order predicate calculus. Dynamic Logic is a system of remarkable unity that is theoretically rich as well as of practical value. It can be used for formalizing correctness specifications and proving rigorously that those specifications are met by a particular program. Other uses include determining the equivalence of programs, comparing the expressive power of various programming constructs, and synthesizing programs from specifications.

This book provides the first comprehensive introduction to Dynamic Logic. It is divided into three parts. The first part reviews the appropriate fundamental concepts of logic and computability theory and can stand alone as an introduction to these topics. The second part discusses PDL and its variants, and the third part discusses DL and its variants. Examples are provided throughout, and exercises and a short historical section are included at the end of each chapter.

 

Co mówią ludzie - Napisz recenzję

Nie znaleziono żadnych recenzji w standardowych lokalizacjach.

Spis treści

III
3
IV
5
V
13
VIII
16
IX
22
XI
27
XIII
38
XIV
53
LXVII
255
LXVIII
256
LXIX
259
LXXI
263
LXXII
266
LXXIII
268
LXXIV
270
LXXV
271

XV
63
XVI
64
XVII
67
XVIII
71
XIX
86
XX
102
XXI
119
XXII
120
XXIII
127
XXIV
134
XXVI
145
XXVIII
146
XXIX
147
XXX
152
XXXI
157
XXXIII
158
XXXIV
163
XXXV
164
XXXVI
167
XXXVII
170
XXXVIII
171
XXXIX
173
XL
174
XLI
186
XLII
187
XLIII
188
XLIV
191
XLVI
195
XLVII
199
XLVIII
201
XLIX
202
L
203
LII
209
LV
211
LVII
216
LVIII
220
LIX
224
LX
225
LXI
227
LXIII
228
LXIV
232
LXV
237
LXVI
250
LXXVI
276
LXXVII
277
LXXVIII
281
LXXIX
283
LXXXI
287
LXXXII
291
LXXXIII
297
LXXXIV
298
LXXXVI
301
LXXXVIII
307
LXXXIX
311
XCI
313
XCIII
317
XCIV
324
XCV
325
XCVI
327
XCVIII
333
XCIX
341
CI
343
CII
344
CIII
347
CIV
355
CV
369
CVI
376
CVII
377
CVIII
378
CIX
380
CX
383
CXII
384
CXIII
386
CXIV
389
CXV
391
CXVI
393
CXVII
394
CXVIII
397
CXX
398
CXXI
408
CXXII
415
CXXIII
418
CXXIV
425
CXXV
439
CXXVI
449
Prawa autorskie

Inne wydania - Wyświetl wszystko

Kluczowe wyrazy i wyrażenia

Popularne fragmenty

Strona v - have seen further than others, it is by standing upon the shoulders of giants. —Isaac Newton
Strona xiii - This operation becomes explicit in Dynamic Logic in the form of the program x :=?, called a nondeterministic or wildcard assignment. This is a rather unconventional program, since it is not effective; however, it is quite useful as a descriptive tool. A more conventional way to obtain a square root of y, if it exists, would be the program

Odniesienia do tej książki

Wszystkie wyniki z usługi Książki Google »

Informacje o autorze (2000)

Dexter Kozen is Joseph Newton Pew, Jr., Professor of Engineering in the Computing and Information Science Department at Cornell University.

Jerzy Tiuryn is Professor in the Institute of Computer Science at the University of Warsaw.

Informacje bibliograficzne