Exercise 10.1

Run the implementation and perform some traces.

Exercise 10.2

Implement the existential rule for model generation (Section 10.4.2). [Hint: Mind where you put cuts. Look at the disjunctive rule.]

Exercise 10.3

[Theoretical]

The way we use hbaseList/2 in the universal rule we strictly speaking do not get the full Herbrand base of the branch at the time of the call: We only consider the literals on the branch, hence we can only see constants that occur in literals. Why is this enough?

Exercise 10.4

The way we control the universal rule isn't fully fair (which means that even if we use iterative deepening, we won't truly approximate completeness with our implementation). To understand the problem, let's look at the input formula . In this example our implementation will use up any given QDepth for on the fathers generated from . So it will never have any QDepth left to instantiate with mothers when it reaches . Try out the following call. It consists of two calls to modGenWrite/3, one with QDepth 10 and one with 20 (plus some additional output):

Try it!

modGenWrite(forall(x, man(x)) & (forall(y, exists(z, father(z,y))) & forall(u, exists(v, mother(v,u)))),_,10),nl,nl,write('next:'),modGenWrite(forall(x, man(x)) & (forall(y, exists(z, father(z,y))) & forall(u, exists(v, mother(v,u)))),_,20).

Thus with such input formulae, the QDepth isn't distributed in a fair manner over new individuals coming from all conjuncts. Do you have an idea how to fix this? Can you implement your idea?

Exercise 10.5

[Theoretical]

We say that an additional rule of a calculus is admissible if it doesn't make the calculus incorrect or incomplete. This exercise deals with the admissibility of . It is obvious that our tableaux calculus doesn't become incorrect if we exchange for : We cannot close any tableaux with that we couldn't close with . The reason is that whenver a tableaux remained open with the old -rule, the branch with the new constant remains open if we use the instead. But why does the calculus remain complete? In other words: Why don't we have more tableaux that remain open if we use instead of ?

Exercise 10.6

Give the (sub)tableaux that the derived rules for the existential quantifier given in Section 10.5 abbreviate.