Show Less
Open access

Tableau Methods for Propositional Logic and Term Logic

Series:

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

←222 | 223→Index

R-branch, 127

addition of branches, 128, 169

adequacy of tableau system

CPL, 63

alphabet

S5, 100

CPL, 27

TL, 66

MTL, 190

branch, 168

CPL, 37

TL, 79

S5, 111

branch consequence, 171

branch consequence relation

CPL, 47

TL, 85

S5, 118

branch translation, 215

cardinality of model, 97

closed branch, 169

CPL, 47

TL, 82

S5, 113

closed tableau, 173

CPL, 58, 59

TL

variant two, 92

variant one, 92

S5, 121

closure under tableau rules, 174

S5, 122

compactness, 52

complete tableau, 173

CPL, 58

TL

variant one, 89

variant two, 91

S5, 121

completeness of tableau system, 186

TL, 96

S5, 151

MTL, 206

completeness theorem, 186

consistency theorem

CPL, 51

contradictory set of formulas, 29

core of rule, 166

S5, 116

estimation of cardinality of model, 97,

206

finite branch property, 16, 27

formula, 153

S5, 100

MTL, 191

CPL, 28

TL, 66

function selecting indices, 163

TL, 75

S5, 105

MTL, 195

generation of appropriate model

TL, 93

S5, 125

MTL, 200

input set, 31

interpretation, 159

interpretation of formulas, 159

maximal branch, 170

CPL, 43

←223 | 224→

TL, 80

S5, 117

S5 variant one, 113

maximal branch in the set of branches, 46

measure of the branch complexity of formula

CPL, 38

model

TL, 67

S5, 101

MTL, 191

model appropriate for the set of expressions

TL, 74

S5, 106

MTL, 196

model generated by branch

TL, 93

MTL, 199

S5, 124

Monadic Logic of Predicates, 68

open branch, 169

CPL, 47

TL, 82

S5, 113

open tableau, 173

CPL, 58, 59

TL

variant two, 92

variant one, 92

S5, 121

output set, 31

quasi-maximal branch

S5, 127, 139

redundant application of rule, 33

redundant variant of branch, 172

CPL, 57

TL, 90

S5, 120

relation

equivalence, 101

universal, 101

rule

CPL, 31

TL, 75

S5, 107

fractional notation, 32

rule application, 37

rules

CPL, 31

TL, 76

S5, 107

MTL, 199

semantic consequence, 159

CPL, 29

TL, 67

S5, 103

semantically defined logic, 159

set of conclusions, 31

set of premises, 31

similar set of expressions, 105, 163

strong similarity

S5, 116, 170

substitution, 130

tableau, 172

CPL, 54

TL

variant one, 87

variant two, 87

S5, 119

tableau axiomatization, 20

tableau contradictory set of formulas

CPL, 29

tableau expressions, 161

S5, 104

MTL, 194

TL, 72

tableau inconsistent set of expressions

TL, 73

←224 | 225→

S5, 105

MTL, 195

tableau rules, 167

tableau translation, 217

theorem on the tableau arbitrariness

CPL, 62

truth in model

TL, 67

MTL, 192

S5, 102

valuation of formulas of CPL, 28

valuation of propositional letters, 28

←225 | 226→