The Handbook of Logic in Computer Science is a multi-volume work covering all major areas of application of logic to theoretical computer science. The Handbook comprises six volumes. Each volume contains five or six chapters giving an in-depth overview of one of the major topics in the field. It is the result of many years of co-operative effort by some of the most eminent frontline researchers in the area. It will no doubt be the standard reference work in logic and theoretical computer science for years to come - essential reading for all those interested in theoretical computer science and logic.
Author(s): Samson Abramsky, Dov M Gabbay, Thomas S E Maibaum (eds.)
Publisher: Clarendon Press
Year: 1992
Language: English
Pages: 582
City: Oxford
Term rewriting systems
1 Introduction 2
2 Abstract reduction systems 3
2.1 Basic notions 11
2.2 Disjoint sums of term rewriting systems 19
2.3 A termination proof technique 29
2.4 Completion of equational specifications 40
2.5 An abstract formulation of completion 55
2.6 Unification 62
3 Orthogonal term rewriting systems 69
3.1 Basic theory of orthogonal term rewriting systems 70
3.2 Reduction strategies for orthogonal term rewriting
systems 77
3.3 Sequential orthogonal term rewriting systems 85
4 Conditional term rewriting systems 99
5 References 108
Lambda calculi with types
1 Introduction 118
2 Type-free lambda calculus 120
2.1 The system 121
2.2 Lambda definability 128
2.3 Reduction 134
3 Curry versus Church typing 148
3.1 The system A-»-Curry 148
3.2 The system A—^-Church 156
4 Typing a la Curry 160
4.1 The systems 161
4.2 Subject reduction and conversion 172
4.3 Strong normalization 176
4.4 Decidability of type assignment 182
5 Typing a la Church 192
5.1 The cube of typed lambda calculi 193
5.2 Pure type systems 212
5.3 Strong normalization for the A-cube 230
5.4 Representing logics and data-types 248
5.5 Pure type systems not satisfying normalization 279
Elements of algorithmic proof
1 The theme of the chapter 311
2 Intuitionistic implication 319
3 An algorithmic proof system for intuitionistic implication 327
4 Automated deduction for intuitionistic implication; resource boundness 336
5 Completeness theorems for the restart rules 351
6 Conjunctions and negations 362
7 Disjunction 369
8 Intermediate logics 375
8.1 Appendix to Section 8 383
9 The universal quantifier and the fragment without disjunctions 385
10 Full predicate system 388
11 Conclusion 409
Designing a theorem prover
1 Folderol: a simple theorem prover 416
1.1 Representation of rules 417
1.2 Propositional logic 418
1.3 Quantifiers and unification 420
1.4 Parameters in quantifier rules 421
2 Basic data structures and operations 424
2.1 Terms 424
2.2 Formulae 425
2.3 Abstraction and substitution 426
2.4 Parsing and printing 427
3 Unification 428
3.1 Examples 429
3.2 Parameter dependencies in unification 430
3.3 The environment 431
3.4 The ML code for unification 432
3.5 Extensions and omissions 433
3.6 Instantiation by the environment 434
4 Inference in Folderol 435
4.1 Solving a goal 436
4.2 Selecting a rule 437
4.3 Constructing the subgoals 438
4.4 Goal selection 439
5 Folderol in action 440
5.1 Propositional examples 441
5.2 Quantifier examples 444
5.3 Beyond Folderol: advanced automatic methods 450
6 Interactive theorem proving 452
6.1 The Boyer/Moore theorem prover 453
6.2 The Automath languages 454
6.3 LCF, a programmable theorem prover 455
6.4 Validation-based tactics 456
6.5 State-based tactics 458
6.6 Technical aspects of Isabelle 460
7 Conclusion 461
8 Program listing 461
Modal and temporal logics
1 Introduction 478
1.1 Transition systems 478
1.2 Runs 481
1.3 Computational concerns 485
2 Propositional modal logics 487
2.1 Basics 487
2.2 Minimal modal logic 490
2.3 Correspondence and incompleteness 492
2.4 Dynamic logic 496
2.5 Modal algebras 498
2.6 Decision procedures 501
3 Propositional temporal logics 504
3.1 Between modal and temporal logics 504
3.2 Basics 507
3.3 Linear and branching time 510
3.4 Minimal temporal logics 515
3.5 Classes of models, automata, and correspondence 518
3.6 Families of runs and temporal properties 522
3.7 Decision procedures 522
4 Modal and temporal mu-calculi 526
4.1 Modal and temporal equations 526
4.2 The mu-calculi 528
4.3 Monotonicity and continuity 532
4.4 Minimal mu-calculi 533
4.5 Decision procedures 534
5 Expressiveness 536
5.1 Expressive completeness 536
5.2 a>-regular expressions 540
5.3 Zig-zags, bisimulations, and histories 542
6 Sound and complete axiom systems 545
6.1 Soundness 545
6.2 Canonical models 547
6.3 Points and schedulers 551
