Department of Computer Science
King's College London, Strand, London, WC2R 2LS, UK
Tel: +44 20 7848 2588 Fax: +44 20 7848 2851
King's College London

CS3AUR: Automated Reasoning 2002

Organisational issues


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.)



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).


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.

Learning LaTeX

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).

 last changed on Friday, 15-Apr-2005 14:42:21 CEST by Ulle Endriss