Mathematical Foundation of Computer Science

DHARM

PROPOSITIONAL LOGIC 129

α-formula ß-formula

~ ~ X : α (X ∨ Y) : β

X : α 1 β 1 : X | Y : β 2

(X ∧ Y) : α ~ (X ∧ Y) : β

X : α 1 β 1 : ~ X | ~ Y : β 2

Y : α 2

~ (X ∨ Y) : α (X → Y) : ß

~ X : α 1 β 1 : ~ X | Y : β 2

~ Y : α 2

~ (X → Y) : α The literals like, X or ~ X not occurred in

X : α 1 either α or β-formula.

~ Y : α 2

Fig. 5.26
Let X be any well formed formula (wff) then tableaux for formula X will be defined as
follows,

The tableaux is a tree, where each node of the tree is labeled by some formula the
tableaux has following characteristics.

I.Formula X will be at the label of root.
II.If a path in tableaux contains an α-formula then we may extend this path by putting
either α 1 -formula or α 2 -formula as the son of the leaf (usually we put both formula α 1
and α 2 one after other).
III.If a path in the tableaux contains a β-formula then we may extend this path by
putting formula β 1 as the left child of the leaf of this path and formula β 2 as the right
child of the leaf of this path.
Suppose T is a tableaux (formation tree) for the formula X shown in Fig. 5.27. The
path in the tableaux contains one or more α and/or β-formula/s. If the path contains a α-
formula then this path will extended beyond leaf with additional α 1 and α 2 -formula. Either,
if the path contains a β-formula then this path will extend to β 1 and β 2 -formula as left and
right child respectively beyond leaf. Thus, we obtain the tableaux T 1 that is an immediate
extension of Tree T. Reader must note that in the tableaux T 1 -Rule II or Rule III may be
applied only once.