Exam Prep for COMP 30411 (2007)

This page containes problems (esp. logic problems), questions, and tips to help prepare for the exam.

Tip: Review the Course Work. It would be perfectly reasonable for us to have questions that are parallel to the course work. I.e., that would ask you to do the same or similar tasks on different content.

Tip: Read the papers and related work listed in Moodle. If we had a lecture centered on a paper (e.g., What is KR?) it's worth paying extra attention.

Tip: Conceptual issues are fair game for the exam. For example, it's typically not enough to know the definition of soundness, completeness, and decidability, but to understand why they matter.

Sample logic problems (there are selected answers; you can request more):

For each of the following propositional formulae:

1. negate and convert to clausal form (extra practice to convert the un-negated version)
2. test for satisfiability using resolution
3. convert to negation normal form
4. test for satisfiability using propositional tableau

1. \(\neg p \rightarrow (\neg q \land (r \land \neg s))\)
2. \((p \rightarrow q) \rightarrow (q \rightarrow p)\)
3. \((p \rightarrow q) \land \neg (q \rightarrow p)\)

1. convert to negation normal form
2. test for satisfiability using the ALC tableau
3. covert to predicate logic using only two variables

1. (p some C or r some C) and (r only (not C))
2. p some (r some (s some C)) and p only (r only (s only (not C)))
3. \(\exists R.(C \sqcup D) \sqcap \forall R.(\neg C \sqcup \neg D)\)
4. \(\exists R.(C \sqcup D) \sqcap \neg\exists R.(C \sqcap D)\)

These are not particularly exciting examples in either case. However, they do reflect the sorts of size/complexity constraints we have to keep in mind for example questions. 

Tip: You can test formulae from your ontology developed for CourseWork 2 (if they are in ALC). It's a little different because of not having an empty ABox. You can, of course, test things in Protege4 by creating a single instance of a complex expression. There is also a very nice Javascript tableau prover. BE CAREFUL...it doesn't use the same tableau rules as we do (e.g., it doesn't require NNF; it works for full predicate logic). Still, it can be helpful.

Tip: You should be able to handle at least Prediate logic notation, Manchester Syntax for OWL (up through ALC concepts), and traditional DL, variable free syntax.