Logics and categories for software engineering and artificial intelligence

Start: Tue April 7th (!)

A course by Till Mossakowski and Lutz Schröder at the Universität Bremen 2009.

Organisation

03-05-H-604.54
Category V
Prerequisites: content of 600.01, 600.02, 601.01
ECTS: 6
Monday 13:00 - 15:00 MZH 7250,
Tuesday 13:00 - 15:00 MZH 7250

Language

Lectures are held in English, and the course material and exercise sheets are in English. Students may ask questions and submit exercise sheets in German or English. The oral examination can be taken in German or English.

Topics

Logic is an important tool for many areas of computer science, including formal software development and artificial intelligence. It plays a similar role as calculus plays for physics. However, driven by the needs of applications, like e.g. specification, verification, expert systems, planning, ontologies, there has been a proliferation of a variety of logics.

Category theory and the theory of institutions are a powerful tool to handle this variety of logics. Common features of logics are abstracted, and complex systems and their logical descriptions can be built in a modular fashion using the categorical notion of colimit.

While providing a rather general introduction to abstract logics, the material of this course is illustrated with examples from artificial intelligence. Moreover, tools implementing logics, categories and colimits will be presented as well.

Prerequisites

The course is aimed at advanced students of Computer Science or Applied Computer science, such as diploma's degree students who have passed their mid-degree exams ("Vordiplom"), Bachelor students in their final year and Master students with a background in formal logic. General mathematical skills are assumed.

Exercises and Exam

During the semester, theoretical and practical assignments will be posed. At then end of the semester, there are oral exams.

Course Materials

Lecture notes

Will be available soon.

Software

In the lecture, we will use the Heterogeneous Tool Set (Hets). In the course, we will give some instructions on how to install Hets on you computers. If you own a laptop on which you want to install Hets, carry it with you.
For ontology classification, we will use Protege. For Protege, you will need Java, best would be Sun Java. Moreover, you will need graphviz. On an Ubuntu machine, just type in
```
sudo apt-get install sun-java6-bin graphviz
```
If you are not sure about your default Java version, type in (for Ubuntu):
```
sudo update-alternatives --config java 
```

Bibliography

CASL and HETS

Michel Bidoit, Peter D. Mosses: CASL User Manual. Introduction to Using the Common Algebraic Specification Language. LNCS 2900.
Peter D. Mosses (Ed.): CASL Reference Manual. The Complete Documentation of the Common Algebraic Specification Language. LNCS 2960.
Till Mossakowski, Christian Maeder, Klaus Lüttich: HETS User Guide. Bremen 2008.

Propositional Logic, First Order Logic, Modal Logic

Jon Barwise, John Etchemendy: Language, Proof and Logic. CSLI Publications, 2002.
M. R. Huth, M. D. Ryan: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004 (2nd edition)

Description Logic

Franz Baader, Diego Calvanese, Daniele Nardi, Peter Patel-Schneider: The Description Logic Handbook. Theory, Implementation and Applications. Cambridge University Press, 2003.

Category Theory

Jiri Adámek, Horst Herrlich, George E. Strecker: Abstract and Concrete Categories. The Joy of Cats. Wiley 1990.
Joseph Goguen: A Categorical Manifesto. Mathematical Structures in Computer Science 1 (1991), 49-67.
D. Rydeheard, R.M. Burstall: Computational Category Theory. Prentice Hall 1988.
Razvan Diaconescu: Institution-independent Model Theory. Birkhäuser 2008.

If a books or paper listed here is not available in the university library or on the World Wide Web, please contact the lecturing staff if you need help getting hold of the reference.

Exercise sheets

Author: Dr. Till Mossakowski

Group BKB

Last updated: June 23, 2009