ANU CECS

Details and Contact

- Classical Propositional
Logic: Slides with
overlays (for screen reading)
Slides without overlays
(for printing)

Sketch of completeness proof of propositional resolution - First-Order Logic: Slides with overlays (for screen reading) Slides without overlays (for printing)

Slides 'First-Order Logic'

Slides 'first-order logic'

- Slides, as presented in class (PDF),
- Handout (PDF) (Same contents as slides but formatted more economically, for printing)
- Supplementary notes, as
written on the whiteboard during class.
**Last update on 24/08/2012.**Big thanks to Joseph Chan for typesetting these notes from my hand written script!

- Slides, as presented in class
(PDF),
Lecture notes (PDF) (Same
contents as slides but differently formatted)
same contents as slides used in class
- Some sample proof problems presented in class
- Automated theorem proving software:
- SPASS, a state-of-the-art theorem theorem prover for first-order logic
- Otter,somewhat outdated but well usable and documented (caution: otter does not accept .p files)
- E-Darwin - A Theorem Prover for the Model Evolution Calculus
- TPTP, a problem library for automated theorem proving

Seminar (graduate level), University of Koblenz (in German).

Block lecture, University of Koblenz (in German).

Seminar (graduate level), University of Koblenz (in German).

Seminar (graduate level), University of Koblenz (in German).

"Verification of distributed systems." Graguate-level course given in the summer term 2002 at the University of Koblenz (in German).

- Informatik II.

"Introduction to Computer Science"

Introductory level course to be given in the summer term 2001 at the University of Giessen (in German). - Projektarbeiten im Fortgeschrittenen-Praktikum Informatik

(Universität Giessen)

- Einführung
in die Informatik für IM I.

"Introduction to Computer Science for Information Managers".

Introductory level course given in the winter term 2000/2001 at the University of Koblenz (in German). - Informatik III.

"Introduction to Computer Science."

Introductory level course given in the winter term 2000/2001 at the University of Giessen (in German).

- Verifikation
Verteilter Systeme.

"Verification of distributed systems." Graguate-level course given in the summer term 2000 at the University of Koblenz (in German). - Software Verification.

Graguate-level course given in the fall term 1998 at the University of New Brunswick, Frederiction, New Brunswick, Canada.

Material on other lectures I gave on logic and/or knowledge representation are available on request.

Last modified: Fri Mar 17 10:51:42 EST 2006