Mathematical Foundation of Computer Science

DHARM

130 MATHEMATICAL FOUNDATION OF COMPUTER SCIENCE

a

b

X

X

X

a

a

b

T

a 1 T 1

a 2

T 1

b 1 b 2

Fig. 5.27

Now we shall define few terms of the tableaux on the basis of that we shall take the

decision about the validity of the formula.

Closed Path

If a path in the tableaux contains a formula R and ~ R then path is a closed path (where R is a

formula). A closed path is never extended. We will designate the closed path by putting sign ×

under this path.

Closed Tableaux

If all paths in the tableaux are closed then tableaux is closed.

Open Path

A path that is not closed is an open path.

True Path

For a path if, there exists an interpretation ‘v’ which makes all formulas of this path true then

path is a true path.

Complete Path

A path for which all its formulas are expended is a complete path.

True Tableaux under Interpretation ‘v’

If tableaux contain at least one true path under interpretation ‘v’ then tableaux is a true tableaux

under ‘v’.

(where interpretation means, a particular combination of the truth value of the propositional

variables of the formula)