R-演算：一种信念修正的逻辑（英文版）

Contents
1 Introduction 1
1.1 Belief Revision 1
1.2 R-Calculus 2
1.3 Extending R-Calculus 4
1.4 Approximate R-Calculus 6
1.5 Applications of R-Calculus 7
References 8
2 Preliminaries 11
2.1 Propositional Logic 11
2.1.1 Syntax and Semantics 12
2.1.2 Gentzen Deduction System 13
2.1.3 Soundness and Completeness Theorem 13
2.2 First-Order Logic 16
2.2.1 Syntax and Semantics 16
2.2.2 Gentzen Deduction System 18
2.2.3 Soundness and Completeness Theorem 18
2.3 Description Logic 21
2.3.1 Syntax and Semantics 21
2.3.2 Gentzen Deduction System 23
2.3.3 Completeness Theorem 25
References 27
3 R-Calculi for Propositional Logic 29
3.1 Minimal Changes 31
3.1.1 Subset-Minimal Change 31
3.1.2 Pseudo-Subformulas-Minimal Change 32
3.1.3 Deduction-Based Minimal Change 34
3.2 R-Calculus for S-Minimal Change 34
3.2.1 R-Calculus S for a Formula 34
3.2.2 R-Calculus S for a Theory 37
3.2.3 AGM Postulates A∈for C-Minimal Change 38
3.3 R-Calculus for Minimal Change 40
3.3.1 R-Calculus T for a Formula 40
3.3.2 R-Calculus T for a Theory 44
3.3.3 AGM Postulates A≤for ≤Minimal Change 46
3.4 R-Calculus for F-Minimal Change 48
3.4.1 R -Calculus U for a Formula 49
3.4.2 R-Calculus U for a Theory 54
References 55
4 R-Calculi for Description Logics 57
4.1 R-Calculus for E-Minimal Change 58
4.1.1 R-Calculus sDL for a Statement 58
4.1.2 R -Calculus sDL for a Set of Statements 62
4.2 R-Calculus for Minimal Change 63
4.2.1 Pseudo-Subconcept-Minimal Change 63
4.2.2 R-Calculus TDL for a Statement 65
4.2.3 R-Calculus TDL for a Set of Statements 69
4.3 Discussion on R-Calculus for F s-Minimal Change 71
References 72
5 R-Calculi for Modal Logic 73
5.1 Propositional Modal Logic 74
5.2 R-Calculus SM for Minimal Change 79
5.3 R-Calculus TM for Minimal Change 83
5.4 R-Modal Logic 88
5.4.1 A Logical Language of R-Modal Logic 89
5.4.2 R-Modal Logic 90
References 92
6 R-Calculi for Logic Programming 93
6.1 Logic Programming 93
6.1.1 Gentzen Deduction Systems 94
6.1.2 Dual Gentzen Deduction System 95
6.1.3 Minimal Change 96
6.2 R-Calculus SLP for Minimal Change 97
6.3 R-Calculus TLP for Minimal Change 99
References 103
7 R-Calculi for First-Order Logic 105
7.1 R-Calculus for S-Minimal Change 105
7.1.1 R-Calculus sFOL for a Formula 105
7.1.2 R-Calculus sFOL for a Theory 108
7.2 R-Calculus for Minimal Change 109
7.2.1 R -Calculus T FOL for a Formula 109
7.2.2 R-Calculus TFOL for a Theory 113
References 114
8 Nonmonotonicity of R. Calculus 115
8.1 Nonmonotonic Propositional Logic 116
8.1.1 Monotonic Gentzen Deduction System G1 116
8.1.2 Nonmonotonic Gentzen Deduction System Logic G2 117
8.1.3 Nonmonotonicity of G2 121
8.2 Involvement ofr K A in a Nonmonotonic Logic 123
8.2.1 Default Logic 124
8.2.2 Circumscription 124
8.2.3 Autoepistemic Logic 125
8.2.4 Logic Programming with Negation as Failure 126
8.3 Correspondence Between R- Calculus and Default Logic 128
8.3.1 Transformation from R-Calculus to Default Logic 128
8.3.2 Transformation from Default Logic to R-Calculus 131
References 132
9 Approximate R-Calculus 133
9.1 Finite Injury Priority Method 134
9.1.1 Post's Problem 134
9.1.2 Construction with Oracle 135
9.1.3 Finite Injury Priority Method 136
9.2 Approximate Deduction 138
9.2.1 Approximate Deduction System for First-Order Logic 139
9.3 R-Calculus Fapp and Finite Injury Priority Method 140
9.3.1 Construction with Oracle 140
9.3.2 Approximate Deduction System F app 141
9.3.3 Recursive Construction 143
9.3.4 Approximate R-Calculus Frece 146
9.4 Default Logic and Priority Method 148
9.4.1 Construction of an Extension without Injury 148
9.4.2 Construction of a Strong Extension with Finite Injury Priority Method 150
References 152
10 An Application to Default Logic 153
10.1 Default Logic and Subset-Minimal Change 154
10.1.1 Deduction System SD for a Default 154
10.1.2 Deduction System SD for a Set of Defaults 157
10.2 Default Logic and Pseudo-subformula minimal Change 159
10.2.1 Deduction System TD for a Default 159
10.2.2 Deduction System TD for a Set of Defaults 163
10.3 Default Logic and Deduction-Based Minimal Change 165
10.3.1 Deduction System UD for a Default 165
10.3.2 Deduction System UD for a Set of Defaults 169
References 170
11 An Application to Semantic Networks 171
11.1 Semantic Networks 171
11.1.1 Basic Definitions 172
11.1.2 Deduction System G4 for Semantic Networks 175
11.1.3 Soundness and Completeness Theorem 176
11.2 R-Calculus for C-Minimal Change 181
11.2.1 R-Calculus SN for a Statement 182
11.2.2 Soundness and Completeness Theorem 184
11.2.3 Examples 188
11.3 R-Calculus for Minimal Change 190
11.3.1 R-Calculus TSN for a Statement 190
11.3.2 Soundness and Completeness Th