<< Prev | - Up - | Next >> |

An example tableaux proof.

Let us turn to some examples to back up the theoretical considerations in the last section.

The Logic PLNQ

To make things more interesting, we will use our reasoning procedure with a fragment (which we call *PLNQ* ) of first-order predicate logic that allows us to express simple natural language sentences, without introducing the whole complications of first-order inference. PLNQ ("Predicate Logic with No Quantifiers") is a fragment of first-order logic without variables and quantifiers^{1}

We will first prove the implication ``If Mary loves Bill and John loves Mary then John loves Mary.''. We do this by exhibiting a tableaux proof of the formula

which is equivalent to

if we eliminate the defined connective . By exhaustively applying the inference rules above, we arrive at the following tableaux.

This tableaux has only one branch, which is closed. So the whole tableaux is closed and constitutes a tableaux proof for our implication.

?- Question!

Annotate each of the nodes of the above tableaux with the rule that has been used to add it.

As a second example let us now look at a variant problem

``Mary loves Bill or John loves Mary'' ``John loves Mary''

To prove the entailment in (1) we represent it as an implication (2). Recall that the deduction theorem allows us to do so. We then eliminate the implication, arriving at (3).

Intuitively, (1) does not hold, because in the situation where the antecedent of the implication is true (i.e. Mary loves Bill), John need not love Mary. If we try to prove the entailment using our tableaux method, we get:

By now we've discussed thoroughly that a tableaux proof for a theorem is a *closed* tableaux for its negation. Yet obviously, the tableaux we've just constructed is saturated (so we cannot expand it any further) and *not closed*. In fact, as we've already convinced ourselves above, our initial entailment conjecture doesn't hold, and so there is no tableaux proof for it.

In Section 9.1.3 we will look closer at open tableaux. We will study their relation to models, and basically see that if a tableaux has any branches that are open *and* saturated, we can read off a model for its input formula from each of them. Making the following observation now will help us understand why: The literals on the open branch of the above tableaux (marked green) taken together characterize the situation in which the conjectured entailment fails to hold (namely the situation where Mary loves Bill but John does not love Mary). In other words: They state the ``minimal requirements'' on a model for the (negated) input formula.

<< Prev | - Up - | Next >> |

1. This logic is equivalent to propositional logic in expressivity: atomic formulae take the role of propositional variables.

Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos

Version 1.2.5 (20030212)