Volume 2
Part V Higher-order logic and logical frameworks
Chapter 15. Classical Type Theory ............................. 965
Peter B. Andrews
1 Introduction to type theory ................................ 967
2 Metatheoretical foundations ................................ 977
3 Proof search ............................................... 987
4 Conclusion ................................................. 998
Bibliography .................................................. 999
Index ........................................................ 1005
Chapter 16. Higher-Order Unification and Matching ............ 1009
Gilles Dowek
1 Type Theory and Other Set Theories ........................ 1011
2 Simply Typed A-calculus ................................... 1018
3 Undecidability ............................................ 1024
4 Huet's Algorithm .......................................... 1028
5 Scopes Management ......................................... 1035
6 Decidable Subcases ........................................ 1041
7 Unification in λ-calculus with Dependent Types ............ 1049
Bibliography ................................................. 1054
Index ........................................................ 1061
Chapter 17. Logical Frameworks ............................... 1063
Frank Pfenning
1 Introduction .............................................. 1065
2 Abstract syntax ........................................... 1067
3 Judgments and deductions .................................. 1075
4 Meta-programming and proof search ......................... 1095
5 Representing meta-theory .................................. 1108
6 Appendix: the simply-typed λ-calculus ..................... 1119
7 Appendix: the dependently typed λ-calculus ................ 1123
8 Conclusion ................................................ 1130
Bibliography ................................................. 1135
Index ........................................................ 1145
Chapter 18. Proof-Assistants Using Dependent Type Systems .... 1149
Henk Barendregt and Herman Geuvers
1 Proof checking ............................................ 1151
2 Type-theoretic notions for proof checking ................. 1153
3 Type systems for proof checking ........................... 1180
4 Proof-development in type systems ......................... 1211
5 Proof assistants .......................................... 1223
Bibliography ................................................. 1230
Index ........................................................ 1235
Name index ................................................... 1238
Part VI Nonclassical logics
Chapter 19. Nonmonotonic Reasoning: Towards Efficient
Calculi and Implementations .................................. 1241
Jürgen Dix, Ulrich Furbach, and Ilkka Niemelä
1 General Nonmonotonic Logics ............................... 1244
2 Automating General Nonmonotonic Logics .................... 1260
3 From Automated Reasoning to Disjunctive Logic
Programming ............................................... 1280
4 Nonmonotonic Semantics of Logic Programs .................. 1297
5 Implementing Nonmonotonic Semantics ....................... 1311
6 Benchmarks ................................................ 1332
7 Conclusion ................................................ 1340
Bibliography ................................................. 1341
Index ........................................................ 1352
Chapter 20. Automated Deduction for Many-Valued Logics ....... 1355
Matthias Baaz, Christian G. Fermüller, and Gemot Salzer
1 Introduction .............................................. 1357
2 What is a many-valued logic? .............................. 1358
3 Classification of proof systems for many-valued logics .... 1361
4 Signed logic: reasoning classically about finitely-
valued logics ............................................. 1368
5 Signed resolution ......................................... 1377
6 An example ................................................ 1389
7 Optimization of transformation rules ...................... 1393
8 Remarks on infinitely-valued logics ....................... 1395
Bibliography ................................................. 1396
Index ........................................................ 1401
Chapter 21. Encoding Two-Valued Nonclassical Logics
in Classical Logic ........................................... 1403
Hans Jürgen Ohlbach, Andreas Nonnengart, Maarten de Rijke,
and Dov M. Gabbay
1 Introduction .............................................. 1405
2 Background ................................................ 1410
3 Encoding consequence relations ............................ 1419
4 The standard relational translation ....................... 1423
5 The functional translation ................................ 1440
6 The semi-functional translation ........................... 1455
7 Variations and alternatives ............................... 1465
8 Conclusion ................................................ 1475
Bibliography ................................................. 1477
Index ........................................................ 1484
Chapter 22. Connections in Nonclassical Logics ............... 1487
Arild Waaler
1 Introduction .............................................. 1489
2 Prelude: Connections in classical first-order logic ....... 1491
3 Labelled systems .......................................... 1516
4 Propositional intuitionistic logic ........................ 1528
5 First-order intuitionistic logic .......................... 1545
6 Normal modal logics up to S4 .............................. 1553
7 The S5 family ............................................. 1567
Bibliography ................................................. 1573
Index ........................................................ 1577
Part VII Decidable classes and model building
Chapter 23. Reasoning in Expressive Description Logics ....... 1581
Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini,
and Daniele Nardi
1 Introduction .............................................. 1583
2 Description Logics ........................................ 1586
3 Description Logics and Propositional Dynamic Logics ....... 1593
4 Unrestricted Model Reasoning .............................. 1598
5 Finite Model Reasoning .................................... 1610
6 Beyond Basic Description Logics ........................... 1619
7 Conclusions ............................................... 1626
Bibliography ................................................. 1626
Index ........................................................ 1633
Chapter 24. Model Checking ................................... 1635
Edmund M. Clarke and Bernd-Holger Schlingloff
1 Introduction .............................................. 1637
2 Logical Languages, Expressiveness ......................... 1641
3 Second Order Languages .................................... 1654
4 Model Transformations and Properties ...................... 1670
5 Equivalence reductions .................................... 1681
6 Completeness .............................................. 1689
7 Decision Procedures ....................................... 1700
8 Basic Model Checking Algorithms ........................... 1711
9 Modelling of Reactive Systems ............................. 1724
10 Symbolic Model Checking ................................... 1735
11 Partial Order Techniques .................................. 1751
12 Bounded Model Checking .................................... 1755
13 Abstractions .............................................. 1759
14 Compositionality and Modular Verification ................. 1764
15 Further Topics ............................................ 1767
Bibliography ................................................. 1774
Index ........................................................ 1788
Chapter 25. Resolution Decision Procedures ................... 1791
Christian G. Fermüller, Alexander Leitsch, Ullrich Hustadt,
and Tanel Tammet
1 Introduction .............................................. 1793
2 Notation and definitions .................................. 1794
3 Decision procedures based on ordering refinements ......... 1802
4 Hyperresolution as decision procedure ..................... 1814
5 Resolution decision procedures for description logics ..... 1830
6 Related work .............................................. 1842
Bibliography ................................................. 1843
Index ........................................................ 1847
Part VIII Implementation
Chapter 26. Term Indexing .................................... 1853
R. Sekar, I.V. Ramakrishnan, and Andrei Voronkov
1 Introduction .............................................. 1855
2 Background ................................................ 1859
3 Data structures for representing terms and indexes ........ 1866
4 A common framework for indexing ........................... 1870
5 Path indexing ............................................. 1875
6 Discrimination trees ...................................... 1883
7 Adaptive automata ......................................... 1891
8 Automata-driven indexing .................................. 1900
9 Code trees ................................................ 1908
10 Substitution trees ........................................ 1917
11 Context trees ............................................. 1922
12 Unification factoring ..................................... 1924
13 Multiterm indexing ........................................ 1927
14 Issues in perfect filtering ............................... 1934
15 Indexing modulo AC-theories ............................... 1939
16 Elements of term indexing ................................. 1943
17 Indexing in practice ...................................... 1951
18 Conclusion ................................................ 1955
Bibliography ................................................. 1957
Index ........................................................ 1962
Chapter 27. Combining Superposition, Sorts and Splitting ..... 1965
Christoph Weidenbach
1 What This Chapter is (not) About .......................... 1967
2 Foundations ............................................... 1969
3 A First Simple Prover ..................................... 1973
4 Inference and Reduction Rules ............................. 1981
5 Global Design Decisions ................................... 2000
Bibliography ................................................. 2008
A Links to Saturation Based Provers .......................... 2011
Index ........................................................ 2012
Chapter 28. Model Elimination and Connection Tableau
Procedures ................................................... 2015
Reinhold Letz and Gemot Stenz
1 Introduction .............................................. 2017
2 Clausal Tableaux and Connectedness ........................ 2018
3 Further Structural Refinements of Clausal Tableaux ........ 2036
4 Global Pruning Methods in Model Elimination ............... 2040
5 Shortening of Proofs ...................................... 2049
6 Completeness of Connection Tableaux ....................... 2062
7 Architectures of Model Elimination Implementations ........ 2070
8 Implementation of Refinements by Constraints .............. 2092
9 Experimental Results ...................................... 2102
10 Outlook ................................................... 2107
Bibliography ................................................. 2109
Index ........................................................ 2113
Concept index ................................................ 2115
|
