This third volume of the book series shows R-calculus is a Gentzen-typed deduction system which is non-monotonic, and is a concrete belief revision operator which is proved to satisfy the AGM postulates and the DP postulates. In this book, R-calculus is taken as Tableau-based/sequent-based/multisequent-based to preserve the satisfiability of the Theory/sequent/multisequent to revise, or sequent-based, to preserve the satisfiability of the sequent to revise. The R-calculi for Post and three-valued logic is given.
This book offers a rich blend of theory and practice. It is suitable for students, researchers and practitioners in the field of logic.
Author(s): Wei Li, Yuefei Sui
Series: Perspectives in Formal Induction, Revision and Evolution
Publisher: Springer
Year: 2022
Language: English
Pages: 283
City: Singapore
Preface to the Series
Preface
Contents
1 Introduction
1.1 Three-Valued Logics
1.2 Deduction Systems
1.3 R-Calculi
1.4 More
1.5 Basic Definitions
1.5.1 Post Three-Valued Logic
1.5.2 Post Three-Valued Description Logic
1.5.3 Remarks
1.6 Types of Deduction Rules
1.7 Notations
References
2 Many-Placed Sequents
2.1 Zach's Theorem
2.2 Analysis of Zach's Theorem
2.3 Tableau Proof Systems
2.3.1 Tableau Proof System Tt
2.3.2 Tableau Proof System Tm
2.3.3 Tableau Proof System Tf
2.4 Incompleteness of Deduction System T''
References
3 Modalized Three-Valued Logics
3.1 Bochvar Three-Valued Logic
3.1.1 Basic Definitions
3.1.2 Multisequent Deduction System Mb
3.2 Kleene Three-Valued Logic
3.2.1 Basic Definitions
3.2.2 Gentzen Deduction System Gk
3.3 Łukasiewicz's Three-Valued Logic
3.3.1 Basic Definitions
3.3.2 Tableau Proof System Tl
References
4 Post Three-Valued Logic
4.1 Theories
4.1.1 Tableau Proof System Tt
4.1.2 Tableau Proof System Tm
4.1.3 Tableau Proof System Tf
4.1.4 Transformations
4.1.5 Tableau Proof System Tt
4.1.6 Tableau Proof System Tm
4.1.7 Tableau Proof System Tf
4.2 Sequents
4.2.1 Gentzen Deduction System Gt
4.2.2 Gentzen Deduction System Gm
4.2.3 Gentzen Deduction System Gf
4.2.4 Gentzen Deduction System Gt
4.2.5 Gentzen Deduction System Gm
4.2.6 Gentzen Deduction System Gf
4.3 Multisequents
4.3.1 Gentzen Deduction System M=
4.3.2 Simplified Ms=
4.3.3 Gentzen Deduction System M=
4.3.4 Simplified Ms=
4.3.5 Cut Elimination Theorem
References
5 R-Calculi for Post Three-Valued Logic
5.1 R-Calculus for Theories
5.1.1 R-Calculus Rt
5.1.2 R-Calculus Rt
5.2 R-Calculi East for Sequents
5.2.1 R-Calculus Et
5.2.2 R-Calculus Em
5.2.3 Basic Theorems
5.3 R-Calculi for Multisequents
5.3.1 R-Calculus K=
5.3.2 Simplified K=s
5.3.3 R-Calculus K=
5.3.4 R-Calculus K=s
References
6 Post Three-Valued Description Logic
6.1 Theories
6.1.1 Tableau Proof System St
6.1.2 Tableau Proof System St
6.2 Sequents
6.2.1 Gentzen Deduction System Ft
6.2.2 Gentzen Deduction System Ft
6.3 Multisequents
6.3.1 Gentzen Deduction System L=
6.3.2 Simplified Ls=
6.3.3 Gentzen Deduction System L=
6.3.4 Simplified Ls=
References
7 R-Calculi for Post Three-Valued Description Logic
7.1 R-Calculus for Theories
7.1.1 R-Calculus Qt
7.1.2 R-Calculus Qt
7.2 R-Calculi for Sequents
7.2.1 R-Calculus Dt
7.2.2 R-Calculus Dm
7.3 R-Calculi for Multisequents
7.3.1 R-Calculus J=
7.3.2 Simplified J=s
7.3.3 Simplified J=
References
8 R-Calculi for Corner Multisequents
8.1 Corner Multisequents MQQQ=
8.1.1 Axioms
8.1.2 Deduction Rules
8.1.3 Deduction Systems
8.2 Corner Multisequents MQQQ=
8.2.1 Axioms
8.2.2 Deduction Rules
8.2.3 Deduction Systems
8.3 R-Calculi KQQQ=/KQQQ=
8.3.1 Axioms
8.3.2 Deduction Rules
8.3.3 Deduction Systems
8.4 R-Calculi JQQQ=/JQQQ=
8.4.1 Axioms
8.4.2 Deduction Rules
8.4.3 Deduction Systems
References
9 General Multisequents
9.1 General Multisequents
9.2 Axioms
9.2.1 Axioms for M=/M=
9.2.2 Axioms for L=/L=-Validity
9.3 Deduction Rules
9.4 Deduction Systems
References
10 R-Calculi for General Multisequents
10.1 R-Calculi K=Q1Q2Q3/K=Q1Q2Q3/J=Q1Q2Q3/J=Q1Q2Q3
10.2 Axioms
10.2.1 Axioms for K=Q1Q2Q3/K=Q1Q2Q3
10.2.2 Axioms for J=Q1Q2Q3/J=Q1Q2Q3
10.3 Deduction Rules
10.3.1 R+=
10.3.2 R+=
10.3.3 R-=
10.3.4 R-=
10.4 Deduction Systems
References
