Some questions about strict tableau in propositional calculus (raising from a book by Melvin Fitting)

Question

Recently, I encountered some questions when reading First-Order Logic and Automated Theorem Proving (1st ed - 1990), by Melvin Fitting.

1: confusing definition of strict tableau (page 39 definition 3.14).I can understand if we focus on all branches of the construction of tableau , thus it means that we never apply some rule to same formula more than once in a branch. But how we gain a general description of "strict tableau"?

2:In prolog, we guarantee a strict construction of tableau by simply removing formula we have used in branch. Thus, tableau expansion rule become identical dual clause set reduction rule, then, the construction become the manipulation from ordinary formula to normal form, the number of which yield finite since konig lemma. Finite guarantee it works in prolog.... It seems natural but I feel somewhat ambiguous between the version of "remove" in prolog and construction of strict tableau. Such as, could contradiction occur in some formulas which have removed?...

Briefly, could anyone make some more explicit explanation to me? Wish your help, thanks!

Answer 1

You can see Marcello D'Agostino & Dov Gabbay (editors), Handbook of Tableau Methods (1998): M.D'Agostino, TABLEAU METHODS FOR CLASSICAL PROPOISTIONAL LOGIC, page 70-71.

In the context of Proof-search with Smullyan’s Tableaux, you can see the definition of regular tableaux:

A tableau is said to be regular if no formula occurs more than once in each branch.

Suppose that in the construction of a tableau $\mathcal T$ we come across a branch $\phi$ containing both a node $k$ labelled with a formula $\beta$ and a node $m$ labelled with $\beta_i$ (with i = 1 or i = 2). Among the many useless moves that one can make when applying the tableau rules mechanically, one of the worst consists in applying the $\beta$-decomposition rule to the formula $\beta$ in $\phi$, because one of the two branches generated by the rule application will contain another copy of $\beta_i$. [see graph]

Let us say that a node $k$ subsumes a node $m$ if $m$ is labelled with a formula $\beta$ and $k$ is labelled with one of its components $\beta_i$. We can often spare a large number of branchings if we agree that a node which is subsumed by another node in a given branch $\phi$ is not used in $\phi$ as premiss of an application of the $\beta$-decomposition rule. This is, somehow, implicit in the procedure to construct a completed tableau described [above], if we simply agree that the $\beta$-decomposition rule should not be applied, in a given branch $\phi$, to a $\beta$-formula labelling a node which is already ‘fulfilled’ in $\phi$. It is not difficult to construct examples showing that this obvious ‘economy principle’ in the application of the tableau rules may, on some occasions, shorten proofs (or in general completed tableaux) by an exponential factor.

As far as the propositional rules are concerned, the regularity restriction implies the basic condition called strictness, namely that no formula is used more than once as a premiss of a rule application. Things are different in the first order case for which we refer the reader to R.Letz’s chapter [FIRST-ORDER TABLEAU METHODS] in this Handbook.

I'm in trouble with tree, so I'll try to describe the example.

We want to check if $\{ p \lor q, q \lor r \} \vDash p \land r$. We build a tableau for :

$\{ Tp \lor q, Tq \lor r, Fp \land r \}$.

When we have fulfilled $Tp \lor q$, we have two branches (we have applied a $\beta$-rule), one with $Tp$ as $\beta_1$ and the other with $Tq$ as $\beta_2$.

With the second step, we fulfill $Tq \lor r$; again apply a $\beta$-rule, so we have to branch both the previous branches. But (form left to right) the third branch have already $Tq$; so we may forget of the $\beta_1$ new branch.

With a computer program, you must check if a formula $\beta_i$ is already present and, if so, avoid to write the branch; in this way, the proof-search algorithm can avoid (in case of complex formulas) unnecessary branches.