R-CALCULUS, IV : propositional logic

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. 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