This fourth volume of the book series combines propositional logic and R-calculus for a new point of view to consider belief revision. It gives the R-calculi for propositional logic, description logics, propositional modal logic, logic programming, β-propositional logic, semantic networks, and three
R-Calculus, IV: Propositional Logic
β Scribed by Wei Li, Yuefei Sui
- Publisher
- Springer
- Year
- 2023
- Tongue
- English
- Leaves
- 264
- Series
- Perspectives in Formal Induction, Revision and Evolution
- Category
- Library
No coin nor oath required. For personal study only.
β¦ Synopsis
This fourth volume of the book series combines propositional logic and R-calculus forΒ a new point of view to consider belief revision.Β It gives the R-calculi for propositional logic, description logics, propositional modal logic, logic programming, β-propositional logic, semantic networks, and three-valued logic, etc..Β Applications of R-calculus in logic of supersequentsΒ are also given.
This book offers a rich blend of theory and practice. It is suitable for students, researchers and practitioners in the field of logic.Β
β¦ Table of Contents
Preface toΒ theΒ Series
Preface
Contents
1 Introduction
1.1 Propositional Logic
1.2 Variant Deduction Systems
1.3 R-Calculus
1.4 R-Calculi in This Volume
1.4.1 R-Calculi for Weak Propositional Logics
1.4.2 R-Calculi for Tableau Proof/Gentzen Deduction Systems
1.4.3 R-Calculi for Deduction Systems GQ1Q2/GQ1Q2
1.4.4 R-Calculi for Deduction Systems GQ1iQ2j/GQ1iQ2j
1.4.5 R-Calculi for Deduction Systems GY1Q1iY2Q2j/GY1Q1iY2Q2j
1.5 Applications of R-Calculi
1.5.1 R-Calculus for -Propositional Logic
1.5.2 R-Calculi for Supersequents
1.6 Notations
References
2 R-Calculus for Simplified Propositional Logics
2.1 Weak Propositional Logics
2.1.1 Gentzen Deduction System G
2.1.2 Gentzen Deduction System G
2.1.3 Gentzen Deduction System G
2.1.4 Gentzen Deduction System G
2.1.5 Gentzen Deduction System G
2.1.6 Gentzen Deduction System G
2.2 R-Calculus for Weak Propositional Logics
2.2.1 R-Calculus R
2.2.2 R-Calculus R
2.2.3 R-Calculus R
2.2.4 R-Calculus R
2.2.5 R-Calculus R
2.2.6 R-Calculus R
2.3 Variant Propositional Logics
2.3.1 Gentzen Deduction System Grightarrow
2.3.2 Gentzen Deduction System Grightarrow
2.3.3 Gentzen Deduction System Gotimesoplus
2.3.4 Gentzen Deduction System Goplusotimes
2.4 R-Calculi for Variant Propositional Logics
2.4.1 R-Calculus Rrightarrow
2.4.2 R-Calculus Rrightarrow
2.4.3 R-Calculus Roplusotimes
2.4.4 R-Calculus Roplusotimes
References
3 R-Calculi for Tableau/Gentzen Deduction Systems
3.1 Tableau Proof Systems
3.1.1 Tableau Proof System Tf
3.1.2 Tableau Proof System Tt
3.1.3 Tableau Proof System Tt
3.1.4 Tableau Proof System Tf
3.2 R-Calculi for Theories
3.2.1 R-Calculus Sf
3.2.2 R-Calculus St
3.2.3 R-Calculus St
3.2.4 R-Calculus Sf
3.3 Gentzen Deduction Systems
3.3.1 Gentzen Deduction System Gt
3.3.2 Gentzen Deduction System Gf
3.3.3 Gentzen Deduction System Gt
3.3.4 Gentzen Deduction System Gf
3.4 R-Calculi for Sequents
3.4.1 R-Calculus Rt
3.4.2 R-Calculus Rf
3.4.3 R-Calculus Rt
3.4.4 R-Calculus Rf
3.5 Conclusions
References
4 R-Calculi RQ1Q2/RQ1Q2
4.1 Gentzen Deduction Systems GQ1Q2
4.1.1 Axioms
4.1.2 Deduction Rules
4.1.3 Deduction Systems
4.2 R-Calculi RQ1Q2
4.2.1 Deduction Rules
4.2.2 Axioms
4.2.3 Deduction Systems RQ1Q2
4.3 Gentzen Deduction Systems GQ1Q2
4.3.1 Axioms
4.3.2 Deduction Rules
4.3.3 Deduction Systems
4.4 R-Calculi RQ1Q2
4.4.1 Axioms
4.4.2 Deduction Rules
4.4.3 Deduction Systems RQ1Q2
4.5 Conclusions
References
5 R-Calculi RQ1iQ2j/RQ1iQ2j
5.1 Gentzen Deduction Systems GE 0ast/GE 1ast
5.1.1 Axioms
5.1.2 Deduction Rules
5.1.3 Deduction Systems
5.1.4 Monotonicity of GE 0ast and GA 1ast
5.2 Gentzen Deduction Systems GQ1iQ2j
5.2.1 Axioms
5.2.2 Deduction Rules
5.2.3 Deduction Systems
5.3 R-Calculi RQ1iQ2j
5.3.1 Axioms
5.3.2 Deduction Rules
5.3.3 R-Calculi
5.4 Gentzen Deduction Systems GQ1iQ2j
5.4.1 Axioms
5.4.2 Deduction Rules
5.4.3 Deduction Systems
5.5 R-Calculi RQ1iQ2j
5.5.1 Axioms
5.5.2 Deduction Rules
5.5.3 R-Calculi
5.6 Conclusions
References
6 R-Calculi: RY1Q1iY2Q2j/RY1Q1iY2Q2j
6.1 Variant R-Calculi
6.1.1 R-Calculus Rt
6.1.2 R-Calculus Rf
6.1.3 R-Calculus Qt
6.1.4 R-Calculus Qf
6.1.5 R-Calculus Pt
6.1.6 R-Calculus Pf
6.2 R-Calculi RY1Q1iY2Q2j
6.2.1 Axioms
6.2.2 Deduction Rules
6.2.3 R-Calculi
6.3 R-Calculi RY1Q1iY2Q2j
6.3.1 Axioms
6.3.2 Deduction Rules
6.3.3 R-Calculi
6.4 Conclusions
References
7 R-Calculi for Supersequents
7.1 Supersequents
7.1.1 Supersequent Gentzen Deduction System G+
7.2 Reduction of Supersequents to Sequents
7.2.1 Gentzen Deduction System Gft
7.2.2 Gentzen Deduction System Gff
7.3 R-Calculus R+
7.3.1 Rft
7.3.2 Rff
7.4 Gentzen Deduction System G-
7.5 Reduction of Supersequents to Sequents
7.5.1 Gentzen Deduction System Gff
7.5.2 Gentzen Deduction System Gft
7.6 R-Calculus R-
7.6.1 Rff
7.6.2 Rft
7.7 Conclusions
References
8 R-Calculi for -Propositional Logic
8.1 -Propositional Logic
8.1.1 Basic Definitions
8.2 Tableau Proof Systems
8.2.1 Tt
8.2.2 Tf
8.2.3 Tableau Proof Systems Tt/Tf
8.3 R-Calculi Rast
8.3.1 R-Calculus Rt
8.3.2 R-Calculus Rf
8.4 Other Minimal Changes
8.4.1 R-Calculus Rt
8.4.2 R-Calculus Qt
8.4.3 R-Calculus Pt
8.5 Gentzen Deduction Systems
8.5.1 Sequents
8.5.2 Gentzen Deduction System Gt
8.6 R-Calculi
8.6.1 R-Calculus Rt
8.6.2 R-Calculus Qt
8.6.3 R-Calculus Pt
8.7 Conclusions
References
π SIMILAR VOLUMES
<p><p>The book is about Gentzen calculi for (the main systems of) modal logic. It is divided into three parts. In the first part we introduce and discuss the main philosophical ideas related to proof theory, and we try to identify criteria for distinguishing good sequent calculi. In the second part
This book series consists of two parts, decidable description logics and undecidable description logics. It gives the R-calculi for description logics. This book offers a rich blend of theory and practice. It is suitable for students, researchers and practitioners in the field of logic.
<p><span>This second volume of the book series shows R-calculus is a combination of one monotonic tableau proof system and one non-monotonic one. The R-calculus is a Gentzen-type deduction system which is non-monotonic, and is a concrete belief revision operator which is proved to satisfy the AGM po