The Lab exercise at `http://www.cs.man.ac.uk/~horrocks/Teaching/cs646/Labs/dlreasoning.html`illustrates
the kind of question that might be asked in the exam. Below is
another example of the kind of exam question you can expect from
the Logic and Reasoning part of the course.

- Given a knowledge base
, explain how would you use a
reasoner capable of deciding knowledge base satisfiability to
determine if:
- (i.e., if is satisfiable with respect to );
- (i.e., if is an instance of with respect to );
- (i.e., if is related to by role with respect to ).

- Explain the basic principals of a tableau algorithm for
, illustrating your answer
by showing how such an algorithm would prove the satisfiability or
unsatisfiability of the following concept:
- For each of the following DL concepts, say if they are
satisfiable and, in the case that they are satisfiable, give an
interpretation in which the extension of the concept is non-empty
(assume that all roles are
**not**transitive:

This document was generated using the
**LaTeX**2`HTML`
translator Version 2002 (1.62)

Copyright © 1993, 1994, 1995, 1996,
Nikos
Drakos, Computer Based Learning Unit, University of
Leeds.

Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.

The command line arguments were:

**latex2html** `-numbered_footnotes -split 0
dlreasoning2`

The translation was initiated by Ian Horrocks on 2003-12-05