Author(s): Donald W. Loveland, Richard E. Hodel, S. G. Sterrett
Publisher: Princeton University Press
Year: 2014
Language: English
Pages: 339
Tags: Информатика и вычислительная техника;Искусственный интеллект;
Cover......Page 1
Title......Page 4
Copyright......Page 5
Contents......Page 6
Preface......Page 10
Acknowledgments......Page 14
PART 1. Proof Theory......Page 18
1 Propositional Logic......Page 20
1.1 Propositional Logic Semantics......Page 22
1.2 Syntax: Deductive Logics......Page 30
1.3 The Resolution Formal Logic......Page 31
1.4 Handling Arbitrary Propositional Wffs......Page 43
2 Predicate Logic......Page 48
2.1 First-Order Semantics......Page 49
2.2 Resolution for the Predicate Calculus......Page 57
2.2.1 Substitution......Page 58
2.2.2 The Formal System for Predicate Logic......Page 62
2.2.3 Handling Arbitrary Predicate Wffs......Page 71
3 An Application: Linear Resolution and Prolog......Page 78
3.1 OSL-Resolution......Page 79
3.2 Horn Logic......Page 86
3.3 Input Resolution and Prolog......Page 94
Appendix A: The Induction Principle......Page 98
Appendix B: First-Order Valuation......Page 99
Appendix C: A Commentary on Prolog......Page 101
References......Page 108
PART 2. Computability Theory......Page 110
4.1 Decision Problems and Algorithms......Page 112
4.2 Three Informal Concepts......Page 124
5.1 Register Machines and RM-Computable Functions......Page 140
5.2 Operations with RM-Computable Functions; Church-Turing Thesis; LRM-Computable Functions......Page 153
5.3 RM-Decidable and RM-Semi-Decidable Relations; the Halting Problem......Page 161
5.4 Unsolvability of Hilbert’s Decision Problem and Thue’s Word Problem......Page 171
6.1 Recursive Functions and the Church-Turing Thesis......Page 182
6.2 Recursive Relations and RE Relations......Page 192
6.3 Primitive Recursive Functions and Relations; Coding......Page 204
6.4 Kleene Computation Relation Tn(e, a1, . . . , an, c)......Page 214
6.5 Partial Recursive Functions; Enumeration Theorems......Page 220
6.6 Computability and the Incompleteness Theorem......Page 233
List of Symbols......Page 236
References......Page 237
PART 3. Philosophical Logic......Page 238
7.1 Alternatives to Classical Logic vs. Extensions of Classical Logic......Page 240
7.2.1 The (So-Called) “Paradoxes of Implication”......Page 245
7.2.2 Material Implication and Truth Functional Connectives......Page 251
7.2.3 Implication and Relevance......Page 255
7.2.4 Revisiting Classical Propositional Calculus: What to Save,What to Change, What to Add?......Page 257
8.1 Fitch’s Natural Deduction System for Classical Propositional Logic......Page 260
8.2 Revisiting Fitch’s Rules of Natural Deduction to Better Formalize the Notion of Entailment—Necessity......Page 268
8.3 Revisiting Fitch’s Rules of Natural Deduction to Better Formalize the Notion of Entailment—Relevance......Page 270
8.4 The Rules of System FE (Fitch-Style Formulation of the Logic of Entailment)......Page 278
8.5 The Connective “Or,” Material Implication, and the Disjunctive Syllogism......Page 298
9.1 Interpretations, Valuations, and Many Valued Logics......Page 305
9.2 Contexts in Which This Four-Valued Logic Is Useful......Page 307
9.3 The Artificial Reasoner’s (Computer’s) “State of Knowledge”......Page 308
9.4 Negation in This Four-Valued Logic......Page 312
9.5 Lattices: A Brief Tutorial......Page 314
9.6 Finite Approximation Lattices and Scott’s Thesis......Page 319
9.7 Applying Scott’s Thesis to Negation, Conjunction, and Disjunction......Page 321
9.8 The Logical Lattice L4......Page 324
9.9 Intuitive Descriptions of the Four-Valued Logic Semantics......Page 326
9.10 Inferences and Valid Entailments......Page 329
10 Some Concluding Remarks on the Logic of Entailment......Page 332
References......Page 333
Index......Page 336