Monday, December 7, 2015

Sample solutions (Tableaux)

I compiled one sample solution for the FOL tableaux from exercise sheet 5, thanks to Jan for his template.

And I've found another extensive example for the Mad Cow DL tableaux from exercise sheet 6, it is in German but you hopefully don't mind.

You can find both in the material folder.


  1. There seems to be quite some inconsistencies on how the Tableaux algorithm gets applied. This results in two questions:

    1. Are we allowed to transform the Knowledge Base with equivalent transformations or implications? (This is done in the linked examples. And it is not necessary.)

    2. The slides (3.10 Slide 7 / 8) show an instance getting pulled out of thin air. This is actually not possible since this would assume that instances exists but the KB might just not contain that specific example. Instead, the rule that gets added to the KB T on Slide 7 seems to be wrong (judging by how a proof for subsumption should be done in

    1. Q1. As said in the lab course, since we are doing logics, you can perform any valid transformation of the statements before starting the tableau.

      Q2. Following the textbook, you should add (Professor⊓¬Person)(a) to the knowledge base, instead of instantiating it in the tableau. The effect is the same. Stick to the reduction of problems of inference to unsatisfiability (3.8 Slides 6 & 7) to be safe!