Seminar Geometrische Logik
Veranstalter: Peter Schuster, Helmut Schwichtenberg und Albert Ziegler
Zeit: Blockseminar, 9.-13. Februar 2009
Ort: Im
Aurachhof (Fischbachau). Abfahrt Sonntag, 8. Februar, 16:42 ab Hauptbahnhof, BOB Richtung Bayerischzell. Ankunft in Fischbachau um 17:49.
Thema: Geometrische Logik.
Sprechstunde Schwichtenberg: Mi 14-15, Zimmer B415.
Bei Interesse an Teilnahme wende man sich bitte unverbindlich an einen der
Organisatoren, zum Beispiel
Albert Ziegler.
Inhalt
Geometric formulas occur naturally in various areas of mathematics:
general topology, algebra, and also in computer science. They allow
for a particularly simple analysis of the computational content of
proofs. We want to understand various conservativity results of
classical over intuitionistic logic concerning geometric formulas as
well as theories. In doing so we shall mainly concentrate on
syntactic methods.
Scheine
Bitte geben Sie ein ausgefülltes
Scheinformular
bei Albert Ziegler oder Frau Bach (Zi. B416) ab. Die Seminarscheine
werden nicht benotet.
Vorträge
- 1. Geometrische Aussagen und Frames als Modelle (Vickers: Topology via
Logic, Kap 2&3):
Max Tschaikowski
- 2. Frames als Algebren (Vickers: Topology via Logic, Kap 4):
Johanna Stelz
- 3. Frames und Topologie (Vickers: Topology via Logic, Kap 5):
Lucia Albers
- 4. Transformation von klassischen Beweisen (Schwichtenberg):
Laura Kuttnig
- 5 a. Barrs Theorem (Negri, von Plato, Kap 8):
Sebastian Huber
- 5 b. Barrs Theorem (alternativer Beweis):
Christoph Senjak
- 6. Geometrische Beweise geometrischer Formeln (Coquand: Completeness):
Matthias Hofer
- 7. Intuitionistische und klassische Beweisbarkeit geometrischer
Sätze (Palmgren):
Florian Müller
- 8. Geometrische und Cogeometrische Theorien
(Negri, von Plato, Kap 9.1-9.3):
Alexander Engel
- 9, 10 Geometrische Logik in der Graphentheorie (Bezem, Coquand):
Philip Seifert
- 11. Die Automatisierung von Hessenbergs Theorem (Bezem, Hendriks):
Korbinian Glaser
- 12-14 Geometrische Beweise in der Algebra (Coste, Lombardi, Roy):
Michael Fuchs, Harald Kümmerle, Karolina Vocke
Weitere Teilnehmer mit Sonderaufgaben:
Matthias Benkard,
Simon Huber,
Basil Karadais
Literatur
Marc Bezem and Thierry Coquand: Newman's Lemma -
a Case Study in Proof Automation and Geometric Logic
Available online, 2003.
Marc Bezem and Thierry Coquand. Automating Coherent Logic. In G. Sutcliffe
and A. Voronkov, editors,
Proceedings LPAR-12, LNCS 3835, pages
246-260, Springer-Verlag, Berlin, 2005.
Marc Bezem & Dimitri Hendriks,
On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic
Available online
Thierry Coquand: A completeness proof for geometric logic
Available online, 2003.
Part III of Sara Negri and Jan von Plato: Proof Analysis
Book Manuscript, 2008
Erik Palmgren: An Intuitionistic Axiomatization of Real Closed Fields
Mathematical Logic Quarterly 48 (2) (2002), pp. 297 - 299.
Helmut Schwichtenberg: Minimal from classical proofs. Proceedings CSL'91,
LNCS 626 (1992),
326-328.
Available online
Steven Vickers: Topology Via Logic
Cambridge University Press, 1989,
ISBN 0521360625, 9780521360623
Helmut Schwichtenberg
[Stand 26. Februar 2009]