博文
[转载]R-CALCULUS: A Logic of Belief Revision（有连接）
|||
R-CALCULUS: A Logic of Belief Revision
Wei Li and Yuefei Sui
Springer 2021, ISBN 978-981-16-2943-3, pp. 1-198
R-Calculi for Logic Programming | Springer Nature Link
PREFACE
There are two kinds of research on belief revision: (1) one is to build a set of postulates that a reasonable belief revision operator should satisfy, and typical examples are AGM postulates for revising a belief base K by a belief A, and DP postulates for iterating revision of a belief base K by a sequence A1,...,An of beliefs; and (2) another is to define a concrete belief revision operator which satisfies the AGM postulates and the DP postulates.
R-calculus is a Gentzen-typed deduction system which is nonmonotonic, and is a concrete belief revision operator which is proved to satisfy the AGM postulates and the DP postulates. This book is to extend R-calculus
(i) from first-order logic to propositional logic, description logics, modal logic and logic programming;
(ii) from minimal change semantics to subset minimal change, pseudo-subformula minimal change and deduction-based minimal change (the last two minimal changes are newly defined);
and prove soundness and completeness theorems with respect to these minimal changes in these logics. To make R-calculus computable, we gave an approximate R-calculus which uses finite injury priority method in recursion theory. Moreover, two applications of R-calculus are given to default theory and semantic inheritance networks.
One goal of this book is to give a roadmap for researching in theoretic computer science by showing how a simple idea (R-calculus) is developed into a series of more and more complicated theories and immersed into other theories, such as default logic, semantic inheritance networks, etc. From R-calculus, we deleted the requirement that Δ is a set of atoms and developed R into S with ⊆-minimal change; with an idea to preserve as much as possible subformulas of formulas to be revised, we developed S into T with ≼-minimal change; after T we could develop U with deduction-based minimal change and different R-calculi for different logics and purposes.
Li Wei, Sui Yuefei
2016,10,30
Contents
1 Introduction 11
1.1 Belief revision . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.2 R-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.3 Extending R-calculus . . . . . . . . . . . . . . . . . . . . . . . 13
1.4 Approximate R-calculus . . . . . . . . . . . . . . . . . . . . . 16
1.5 Applications of R-calculus . . . . . . . . . . . . . . . . . . . . 17
2 Preliminaries 21
2.1 Propositional logic . . . . . . . . . . . . . . . . . . . . . . . . 21
2.1.1 Syntax and semantics . . . . . . . . . . . . . . . . . . 22
2.1.2 Gentzen deduction system . . . . . . . . . . . . . . . . 22
2.1.3 Soundness and completeness theorem . . . . . . . . . 23
2.2 First-order logic . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.2.1 Syntax and semantics . . . . . . . . . . . . . . . . . . 26
2.2.2 Gentzen deduction system . . . . . . . . . . . . . . . . 27
2.2.3 Soundness and completeness theorem . . . . . . . . . 28
2.3 Description logic . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.3.1 Syntax and semantics . . . . . . . . . . . . . . . . . . 31
2.3.2 Gentzen deduction system . . . . . . . . . . . . . . . . 32
2.3.3 Completeness theorem . . . . . . . . . . . . . . . . . . 34
3 R-calculi for Propositional Logic 39
3.1 Minimal changes . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.1.1 Subset-minimal change . . . . . . . . . . . . . . . . . . 41
3.1.2 Pseudo-subformulas-minimal change . . . . . . . . . . 42
3.1.3 Deduction-based minimal change . . . . . . . . . . . . 44
3.2 R-calculus for ⊆-minimal change . . . . . . . . . . . . . . . . 44
3.2.1 R-calculus S for a formula . . . . . . . . . . . . . . . . 44
3.2.2 R-calculus S for a theory . . . . . . . . . . . . . . . . 47
3.2.3 AGM postulates A⊆ for ⊆-minimal change . . . . . . 48
3.3 R-calculus for ≼-minimal change . . . . . . . . . . . . . . . . 50
3.3.1 R-calculus T for a formula . . . . . . . . . . . . . . . 50
3.3.2 R-calculus T for a theory . . . . . . . . . . . . . . . . 54
3.3.3 AGM postulates A≼ for ≼-minimal change . . . . . . 55
3.4 R-calculus for ⊢≼-minimal change . . . . . . . . . . . . . . . . 58
3.4.1 R-calculus U for a formula . . . . . . . . . . . . . . . 58
3.4.2 R-calculus U for a theory . . . . . . . . . . . . . . . . 63
4 R-calculi for description logics 66
4.1 R-calculus for ⊆-minimal change . . . . . . . . . . . . . . . . 67
4.1.1 R-calculus S DL for a statement . . . . . . . . . . . . . 67
4.1.2 R-calculus S DL for a set of statements . . . . . . . . . 71
4.2 R-calculus for ≼-minimal change . . . . . . . . . . . . . . . . 72
4.2.1 Pseudo-subconcept-minimal change . . . . . . . . . . . 72
4.2.2 R-calculus TDL for a statement . . . . . . . . . . . . 74
4.2.3 R-calculus TDL for a set of statements . . . . . . . . . 78
4.3 Discussion on R-calculus for ⊢≼-minimal change . . . . . . . 79
5 R-calculi for modal logic 82
5.1 Propositional modal logic . . . . . . . . . . . . . . . . . . . . 82
5.2 R-calculus SM for ⊆-minimal change . . . . . . . . . . . . . . 88
5.3 R-calculus TM for ≼-minimal change . . . . . . . . . . . . . . 92
5.4 R-modal logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
5.4.1 A logical language of R-modal logic . . . . . . . . . . 98
5.4.2 R-modal logic . . . . . . . . . . . . . . . . . . . . . . . 99
6 R-calculi for logic programming 102
6.1 Logic programming . . . . . . . . . . . . . . . . . . . . . . . . 102
6.1.1 Gentzen deduction systems . . . . . . . . . . . . . . . 103
6.1.2 Dual Gentzen deduction system . . . . . . . . . . . . . 104
6.1.3 Minimal change . . . . . . . . . . . . . . . . . . . . . . 105
6.2 R-calculus S LP for ⊂-minimal change . . . . . . . . . . . . . . 106
6.3 R-calculus TLP for ≼-minimal change . . . . . . . . . . . . . 108
7 R-calculi for first-order logic 113
7.1 R-calculus for ⊆-minimal change . . . . . . . . . . . . . . . . 113
7.1.1 R-calculus S FOL for a formula . . . . . . . . . . . . . . 113
7.1.2 R-calculus S FOL for a theory . . . . . . . . . . . . . . 115
7.2 R-calculus for -minimal change . . . . . . . . . . . . . . . . 117
7.2.1 R-calculus TFOL for a formula . . . . . . . . . . . . . 117
7.2.2 R-calculus TFOL for a theory . . . . . . . . . . . . . . 121
8 Nonmonotonicity of R-calculus 123
8.1 Nonmonotonic propositional logic . . . . . . . . . . . . . . . . 124
8.1.1 Monotonic Gentzen deduction system G’1 . . . . . . . 124
8.1.2 Nonmonotonic Gentzen deduction system logic G2 . . 125
8.1.3 Nonmonotonicity of G2 . . . . . . . . . . . . . . . . . 129
8.2 Involvement of Γ⊬ A in a nonmonotonic logic . . . . . . . . . 131
8.2.1 Default logic . . . . . . . . . . . . . . . . . . . . . . . 132
8.2.2 Circumscription . . . . . . . . . . . . . . . . . . . . . 132
8.2.3 Autoepistemic logic . . . . . . . . . . . . . . . . . . . 133
8.2.4 Logic programming with negation as failure . . . . . . 134
8.3 Correspondence between R-calculus and default logic . . . . . 135
8.3.1 Transformation from R-calculus to default logic . . . . 136
8.3.2 Transformation from default logic to R-calculus . . . . 138
9 Approximate R-calculus 141
9.1 Finite injury priority method . . . . . . . . . . . . . . . . . . 141
9.1.1 Post’s problem . . . . . . . . . . . . . . . . . . . . . . 142
9.1.2 Construction with oracle . . . . . . . . . . . . . . . . . 143
9.1.3 Finite injury priority method . . . . . . . . . . . . . . 144
9.2 Approximate deduction . . . . . . . . . . . . . . . . . . . . . 146
9.2.1 Approximate deduction system for first-order logic . . 147
9.3 R-calculus F app and finite injury priority method . . . . . . . 147
9.3.1 Construction with oracle . . . . . . . . . . . . . . . . . 147
9.3.2 Approximate deduction system F app . . . . . . . . . . 149
9.3.3 Recursive construction . . . . . . . . . . . . . . . . . . 151
9.3.4 Approximate R-calculus F rec . . . . . . . . . . . . . . 154
9.4 Default logic and priority method . . . . . . . . . . . . . . . . 156
9.4.1 Construction of an extension without injury . . . . . . 156
9.4.2 Construction of a strong extension with finite injury priority method . . . . . . . . . . . . . . . . . . . . . . 157
10 An application to default logic 161
10.1 Default logic and subset-minimal change . . . . . . . . . . . . 162
10.1.1 Deduction system S D for a default . . . . . . . . . . . 162
10.1.2 Deduction system S D for a set of defaults . . . . . . . 165
10.2 Default logic and pseudo-subformula-minimal change . . . . . 167
10.2.1 Deduction system TD for a default . . . . . . . . . . . 167
10.2.2 Deduction system TD for a set of defaults . . . . . . . 171
10.3 Default logic and deduction-based minimal change . . . . . . 172
10.3.1 Deduction system UD for a default . . . . . . . . . . . 173
10.3.2 Deduction system UD for a set of defaults . . . . . . . 176
11 An application to semantic networks 178
11.1 Semantic networks . . . . . . . . . . . . . . . . . . . . . . . . 178
11.1.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . 179
11.1.2 Deduction system G4 for semantic networks . . . . . . 182
11.1.3 Soundness and completeness theorem . . . . . . . . . 183
11.2 R-calculus for ⊆-minimal change . . . . . . . . . . . . . . . . 188
11.2.1 R-calculus S SN for a statement . . . . . . . . . . . . . 189
11.2.2 Soundness and completeness theorem . . . . . . . . . 191
11.2.3 Examples . . . . . . . . . . . . . . . . . . . . . . . . . 195
11.3 R-calculus for ≼-minimal change . . . . . . . . . . . . . . . . 196
11.3.1 R-calculus TSN for a statement . . . . . . . . . . . . . 197
11.3.2 Soundness and completeness theorem of TSN . . . . . 198
https://blog.sciencenet.cn/blog-3653970-1524806.html
下一篇：[转载]R-CALCULUS, IV: Propositional Logic（含链接）
