Geomeetrilise loogika teooria ja rakendused (kevad 2005)
Registreerumine: Kursusele registreerumiseks deklarareerida selle kuulamine vastavalt kehtivale korrale dekanaadis, kuid saata ka meil Tarmo Uustalule. Tähtaeg: 7.2.2005.
Kood: ITT9201
Punkte: 1.5
Tunde: 10 tundi loenguid
Tunniplaan: loengud N 17.2. kl 14-15.30, R 18.2 kl 12-13.30, E 21.2. kl 14-15.30, T 22.2. kl 14-15.30, K 23.2. kl 14-15.30 Küberneetika Maja (Akadeemia tee 21) ruumis B101
Kontrollivorm: eksam
Eksam: Eksamihinde saamiseks tuleb lahendada suurem komplekt koduülesandeid [pdf]. Tähtaeg N 24.3.2005!
Õppejõud: prof Marc Bezem, Dept. of Informatics, University of Bergen
Kontakt: bezem(at)ii.uib.no, tarmo(at)cs.ioc.ee, 620 4250
Kursus toimub EITSA administreeritava riikliku programmi Tiigriülikool toel.
Theory and practice of (first-order) geometric logic
Abstract
Geometric logic (GL) is the logic preserved by geometric morphisms between topoi. The first-order fragment of GL extends resolution logic in that geometric clauses can have existentially quantified conclusions. A substantial number of reasoning problems (e.g., in confluence theory, lattice theory and projective geometry) can be formulated directly in GL without any skolemization. Thus no skolem axioms are necessary and the proofs are direct and constructive. These advantages can outweigh the disadvantage that a more expressive logic is generally more difficult to implement than a simpler one. We explore the balance between the advantages and disadvantages with an implementation in the programming language Prolog of (incomplete) proof search in GL including the generation of proof objects. If a proof has been obtained it can be verified directly in the proof assistant Coq.
Lecture plan:
- From (Horn) Clauses to Geometric Formulae. Proof System
- Semantics and Completeness
- Prolog Implementation Aspects (small case studies)
- Inductive Proofs in Confluence Theory (larger case study)
- Odds & Ends: undecidability, generation of proof objects, large case study in projective geometry...
Course material
- M. Bezem. A depth-first implementation of geometric logic in Prolog. Overview slides. [pdf]
- M. Bezem. Completeness and undecidability of geometric logic. A note. [ps.gz]
- M. Bezem, T. Coquand. Newman's lemma - a case study in proof automation and geometric logic. Bull. of EATCS, v. 79, pp. 86-100, 2003. // Also in G. Paun, G. Rozenberg, A. Salomaa, eds, Current Trends in Theoretical Computer Science, v. 2, pp. 267-282. World Scientific, Singapore, 2004. [ps.gz]
- The prover implementation [tar.gz] (password protected).
Useful links
Tarmo Uustalu
Viimane uuendus 22.2.2005