Show Less
Open access

Tableau Methods for Propositional Logic and Term Logic


Tomasz Jarmużek

The book aims to formalise tableau methods for the logics of propositions and names. The methods described are based on Set Theory. The tableau rule was reduced to an ordered n-tuple of sets of expressions where the first element is a set of premises, and the following elements are its supersets.

Show Summary Details
Open access





1.1Tableau methods

1.2Terminology and problems in the book

1.2.1Study schedule and goals

1.2.2Terminology and issues in the book

1.3Notations and concepts of the set theory

2Tableau system for Classical Propositional Logic

2.1Introductory remarks

2.2Language and semantics

2.3Basic concepts of the tableau system for CPL

2.3.1Tableau rules for CPL

2.3.2Branches for CPL

2.3.3Maximal branches

2.3.4Closed and open branches

2.3.5Branch consequence relation

2.4Relations of semantic consequence and branch consequence

2.4.1Soundness theorem

2.4.2Completeness theorem

2.5Tableaux for CPL vs. semantic consequence relation


3Tableau system for Term Logic

3.1Introductory remarks

3.2Language and semantics

3.3Basic concepts of the tableau system for TL

3.3.1Tableau rules for TL

3.3.2Branches for TL

3.3.3Maximal branches

3.3.4Closed and open branches

3.3.5Relation of branch consequence

3.4Tableaux for TL

3.5Completeness theorem for the tableau system for TL

3.5.1Estimation of cardinality of model for TL

4Tableau system for modal logic S5

4.1Introductory remarks

4.2Language and semantics

4.3Basic concepts of the tableau system for S5

4.3.1Tableau rules for S5

4.3.2Branches for S5

4.3.3Closed and open branches

4.3.4Maximal branches

4.3.5Relation of branch consequence

4.4Tableaux for S5

4.5Theorem on the completeness of the tableau system for S5

5Metatheory of tableau systems for propositional logic and term logic

5.1Introductory remarks

5.2Language and semantics

5.3Basic concepts of the tableau system

5.4Tableau rules


5.4.2Closed and open branches

5.4.3Maximal branches

5.4.4Branch consequence relation


5.6Completeness theorem

6Examples of applications

6.1Introductory remarks

6.2Tableau system for Modal Term Logic de re



6.2.4Tableau expression

6.2.4Rules for the tableau system for logic MTL

6.2.5Branches and tableaux for MTL

6.2.6Theorem on the completeness of the tableau system for MTL

6.2.7Estimation of cardinality of model for MTL

6.3Tableau systems for modal logics

6.3.1Language and semantics

6.3.2Tableau expressions

6.3.3Rules, branches and tableaux for modal logics

6.3.4Generating of model

6.3.5Completeness theorem of tableau systems for modal logics

6.4Tableau system

6.5Transition from the formalized tableaux to the standard tableaux