Refutation Methods in Modal Propositional Logic

1 Introduction and Motivation

1.1 Basic Concepts

1.2 From Models to Refutations

1.3 From Refutations to Models

1.4 Refutation Search

I From Models to Syntactic Refutations

2 Syntactic Tools 24

2.1 Propositional Formulas

2.2 Boolean Laws

2.3 Classical Refutation System

2.4 Modal Formulas

2.5 Modal Replacement

3 Finite Models

3.1 Normal Modal Logics

3.2 Characteristic Formulas

3.3 The Logics with the FMP

3.4 The Finite-Valued Logics

3.5 A Logic without the FMP

II Normal Form Procedures

4 CL Normal Forms

4.1 Interpretations

4.2 Introducing Normal Forms

4.3 Proof System for Normal Forms

4.4 Refutation System for Normal Forms

4.5 Syntactic Completeness

4.6 Reductions to Normal Forms

5 S5 Normal Forms

5.1 Semantics

5.2 Proof System

5.3 Normal Forms

5.4 Refutation System

5.5 Cluster Models

5.6 Syntactic Completeness

5.7 Reductions to Normal Forms

5.8 Semantic Completeness

6 G Normal Forms

6.1 Semantics

6.2 Proof System

6.3 Normal Forms

6.4 Refutation System

6.5 Syntactic Reductions

6.6 Completeness

6.7 Reductions to Normal Forms

6.8 Constructing Counter-Models

7 GRZ Normal Forms

7.1 Semantics

7.2 Proof System

7.3 Normal Forms

7.4 Refutation System

7.5 Syntactic Reductions

7.6 Completeness

7.7 Reductions to Normal Forms

7.8 Constructing Counter-Models

8 S4DBR Normal Forms

8.1 The Logic S4DBR

8.2 Normal Forms

8.3 Refutation System

8.4 Syntactic Reductions

8.5 Completeness

8.6 Reductions to Normal Forms

8.7 Constructing Counter-Models

9 S4 Normal Forms

9.1 The Logic S4

9.2 Reductions to Normal Forms

9.3 The Logic S4.3

10 Refutation Search

10.1 Classical Logic

10.2 Modal Logic

10.2.1 Completeness

10.2.2 The Logic GRZ

10.2.3 The Logic S4

10.2.4 The Logic S4DBR

10.3 Tableaux