AK der Theoretischen Informatik 3 (in engl.Spr.)

(E 185 Institut für Computersprachen der Technisch-naturwissenschaftliche Fakultät der Technischen Universität Wien, WS 1999/2000)

(see also here)

Automated Theorem Proving in Lattice-Ordered Structures

185.134
AK der Theoretischen Informatik 3 (in engl.Spr.), VU, 2.0 Std. (WS 1999/2000)
(Automated Theorem Proving in Lattice-Ordered Structures)

Lehrveranstaltungsleiter: Viorica Sofronie-Stokkermans, Max-Planck Institut für Informatik, Saarbrücken

Diese Lehrveranstaltung ist Teil des Wahlfachs "AI und theoretische Informatik" des Studiums Informatik.

Inhalt

In the first part of the course we introduce some fundamental notions in automated theorem proving: we recall the main results in resolution and its refinements and in rewriting; then we present superposition and ordered chaining with selection.

The second part presents resolution-based decision procedures for lattice-ordered structures. The method we present generalizes known results from modal logic: It is known that in modal logic two kinds of models can be used: algebraic (Boolean algebras with operators), or Kripke-style (sets endowed with a binary relation). Kripke-style models are more comfortable to use since they have a much simpler structure.

We show that the idea of using relational structures instead of algebras can also be applied to automated theorem proving in classes of distributive lattices with operators. We end with some applications to automated theorem proving in some classes of non-classical logics, especially (multi-)modal logics, intuitionistic logic, some many-valued logics.

The lecture will be structured as follows:

Automated theorem proving: resolution, rewriting (reminder); superposition, ordered chaining with selection.
Automated theorem proving in lattice-ordered structures:
1. (lattice-)ordered structures: lattices, distributive lattices, Heyting algebras and Boolean algebras; representation theorems;
2. a decision procedure for the universal theory of distributive lattices (Boolean algebras, Heyting algebras)
  - structure-preserving translation to clause form
  - decision procedures by ordered chaining with selection
3. Applications to non-classical logics, especially (multi-)modal logics, intuitionistic logic, some many-valued logics.

Vorlesungstermine

Die Vorlesung wird geblockt vom 24. bis 30. Jänner 2000 abgehalten. Die genauen Termine werden bei der Vorbesprechung festgelegt.

Vorbesprechung:

Montag, 24.1.2000, 10:30, Seminarraum E1852
Institut für Computersprachen, Favoritenstraße 9/Stiege 1/3. Stock (gelber Bereich)

Vorkenntnisse

Knowledge about resolution and rewriting would be helpful. (The main notions will be briefly recalled in the first lecture.)

Vorlesungsunterlagen

Will be made available during the lecture.

Beurteilung