Office hours: Mondays 2-3pm and Tuesdays 2-3pm (Room 542).
If you need to see me outside these hours please contact me by email first.
Lectures and tutorials: Mondays 6-7pm (Room 228) and
Tuesdays 11am-1pm (Room 23D).
Please note that, due to the recent changes in the
Departmental curriculum, the syllabus printed in the
undergraduate
course booklet will be modified in this year's edition of the course
to avoid overlaps with the old CS2LAP course.
Coursework for this course unit is compulsory.
Assignments will be marked as good/pass/fail. To pass the course you must pass
all coursework assignments and obtain at least 40% in the examination
paper in May. (Your final mark for the course, however, will be determined by
your examination result alone.)
F. Baader.
Logic-based
Knowledge Representation. In M. Wooldridge and M. Veloso (eds.),
Artificial Intelligence Today: Recent Trends and Developments,
LNCS 1600, pages 13-41, Springer-Verlag, 1999.
Background reading
A major part of the course will be dedicated to automated deduction in
first-order logic with Tableaux and Resolution. The following book is the
standard text in the area and we highly recommend it (although we shall not
follow it very closely in the course).
M. Fitting. First-order Logic and Automated Theorem Proving.
2nd edition, Springer-Verlag, 1996.
WinKE
We will be using the WinKE software to practice
the construction of KE/Tableaux proofs in first-order logic.
To install WinKE (on a computer in the Department or at home) run the setup
program at K:\install\WinKE\winke-setup.exe (under Windows).
This will install the software in the directory C:\WinKE\.
Start by reading the README file.
I recommend to use LaTeX to produce the documentation for
Coursework 2 (or any other scientific document in fact).
The following sample document may be helpful to get started.
Download it, then run latex sample.tex (under Linux),
and finally xdvi sample.dvi &. Other options are
described in the file itself (use emacs or a similar
program to read and manipulate it).