Definition:Extension of Propositional Tableau

This page is about extensions of propositional tableaus. For other uses, see Extension.

Definition

Let $\left({T, \mathbf H, \Phi}\right)$ be a propositional tableau.

Definition 1

A tableau $T'$ is an extension of $T$ if $T'$ can be obtained from $T$ by repeatedly adding nodes to the leaf nodes of $T$ (by means of the tableau extension rules).

Definition 2

An extension of $T$ is a propositional tableau $\left({S, \mathbf H', \Phi'}\right)$ such that:

$S$ is an extension of $T$;

$\mathbf H = \mathbf H'$;

$\Phi'$ is an extension of $\Phi$.

Equivalence of Definitions

That these definitions are equivalent is shown on Equivalence of Definitions of Extension of Propositional Tableau.

Also see

• Definition:Extension of Rooted Tree