The lecturer for this course is  Brandon Bennett  of the  School of Computing.
 

Objectives:

Topics Covered:

• Classical Logic and Inference
• Revision of propositional and 1st-order logic
• A sequent calculus proof system
• Basic model theory
• Soundness, Completeness and Decidability
• Representing and reasoning about time and change
• Tense Logic and 1st-order temporal logic
• AI representaions of time
• Non-monotonic reasoning about change
• Space and physical objects
• Qualitative spatial relationships
• Matter, objects and physical events
• Combining space with time
• Ontology and AI Knowledge Bases
• The need for world knowledge
• Ontology and Ontologies
• Description Logic
• The problem of vagueness

Lectures and Additional Course Material:

The lectures from 2007 can be found here.

Supplementary course material:

• A Concise Introduction to the Fundamentals of Classical Logic (pdf, 2-up pdf), .
• An excersise on translating from English to 1st-order logic (pdf).
• An example using Sequent Calculus to show the inconsistency inherent in Russell's famous set-theoretic paradox (pdf).
• Supplementary (borrowed) lecture notes and slides:
  • Learn Prolog Now! Online notes and tutorial on the Prolog programming language.
  • Knowledge Representation and Reasoning, Leora Morgenstern (course web site)
  • Introduction to the Situation Calculus, Maurice Pagnucco (PDF slides)
  • Introduction to Ontologies and Description Logics, Carlos Areces (PDF slides)
  • From Tableaux to Automata for Description Logics (PDF slides) [Introductory material on slides 1-7 is most relevant]

Example exam papers:

• 2002 paper (PDF)
• 2004 paper (PDF)
• 2005 paper (PDF)
• 2006 paper (PDF)
• 2007 paper (PDF)
• Past paper answers
  I strongly recommend that you make a concerted attempt to answer the questions before looking at the answers, otherwise you will not learn the thought process required to solve the problems on your own. Note that for some questions there may be alternative, equally correct answers.

Online Discussion Groups:

      local.modules.krr      and     local.modules.krr.talk

The first of these is for important announcements about the module.
The second is for you to post any kind of comment or query relating to the module.
 

Coursework:

• Coursework 1 Automated Reasoning -- 20% of total marks for course.
  Set 21st October, Due in 9am, 14th November, 2008.
  To complete this you will need to use both the Prolog implemented Gentzen theorem prover and the Otter theorem prover. See the Software Resources section below for further details about these.
• Coursework 2 (2007) Build your own Ontology -- 20% of total marks for course.
  Set 18th November, Due 9am, 9th December, 2008.
  A sketch of an ontology specification for the domain of Sailing is given here.

Software Resources

• A Prolog Gentzen Theorem Prover
  A Gentzen calculus theorem prover written in Prolog can be found at ~krr/gentzen_prover_2008.pl.
  An exercise explaining how to use it is available here.
• The Otter Theorem Prover
  An executable of the Otter theorem prover is available at ~krr/otter.
  An exercise explaining the basics of using Otter is available here.

Reading Material:

• Computational Intelligence: A Logical Approach, David Poole Alan Mackworth Randy Goebel, OxfordUniversity Press, New York, 1998.
• Russell S and Norvig P (1995), Artificial Intelligence: A Modern Approach, Prentice Hall.
• E Rich and K Knight (1991), Artificial Intelligence (2nd Ed), McGraw Hill.
• M Ginsberg (1994), Essentials of Artificial Intelligence, Morgan Kaufmann.
• T Dean, J Allen and Y Aloimonos (1995), Artificial Intelligence: Theory and Practice, Benjamin Cummins.
• Readings in Knowledge Representation, Editors: R J Brachman and H J Levesque, Morgan Kaufmann, 1985.
• Representations of Commonsense Knowledge, E Davis, Morgan Kaufmann, 1990.

Some useful links:

•  Leeds Qualitative Spatial Reasoning group
• SICStus Prolog user manual
• The RACER Description Logic system
• Otter Theorem Prover
• Enrico Franconi's description logic course
• The Ontology Page
•  Brandon's Ontology Page
• John McCarthy's Home Page