Exercise 9.1

1. Construct a model generation tableaux to represent the following discourse: ``Fido is the dog and Mimi is the cat. Jane owns the dog or Jane owns the cat. Jane does not own Fido.''

2. Now show, using the model generation calculus, that adding the sentence ``Jane does not own Mimi'' to the discourse above leads to a contradiction.

Clarification: We assume that ``the dog'' is mapped to a constant , where the information is in the world knowledge. Likewise for the cat.

Exercise 9.2

Look again at the example in Section 9.1.2. Instead of the somewhat clumsy sentence quoted there, let us now consider a small discourse similar in meaning: ``If John doesn't love Mary then Mary loves Bill. John doesn't love Mary.''. How would our tableaux approach process this discourse? Construct the tableaux.

Compare your tableaux to the one you would build to validate the intuitively correct argument ``If John doesn't love Mary then Mary loves Bill. John doesn't love Mary. Thus Mary loves Bill.''

Exercise 9.3

Project!

[This is a project (mid- or end-term)]

Modify our model generation procedure for PLNQ such that it can process discourse (i.e. multiple sentences) as sketched in Section 9.2.

You may (as in our implementation for single sentences) abstract over the question which is the preferred model (branch). This means that you simply take the first model the implementation generates as the preferred one. In this case Prolog's search strategy, and in particular the order of the two disjunctive clauses of tab/3, effectively determine which model is prefered. The only thing you have to work out is how to store the alternative branches so that they can be backtracked to if subsequent expansions lead to branch closure on the preferred one.

Alternatively, you can re-implement the tableaux procedure such that the tableaux is explicitely represented. There are various ways of doing this: you may e.g. represent a tableaux branch as a list of formulae (and hence a tableaux as a list of lists (branches)). This is what's done in the famous textbook by Melvin Fitting. Or you may assert tableaux nodes to the database and establish the connection between the nodes by specifying the children of each node. Any such explicit representation will give you more freedom in controling the tableaux expansion.