Bonn Mathematical Logic Group

Hauptseminar Angewandte Mathematische Logik (S2A4)

Dozent

Zeit

Automatisches und interaktives Beweisen

Der Gödelsche Vollständigkeitssatz besagt, dass eine Aussage (in der Sprache der Prädikatenlogik erster Stufe) genau dann in allen Strukturen erfüllt ist, wenn sie formal bewiesen werden kann. Damit wird das praktisch unlösbare Problem, sämtliche Strukturen zu überprüfen, auf die Suche nach einer endlichen Ableitung im Sequenzenkalkül reduziert. Eine solche Beweissuche ist im allgemeinen ebenfalls recht komplex, aber im Bereich des automatischen Beweisens wurden logische und technische Methoden entwickelt, die Beweise einfacher mathematischer Aussagen automatisch und mit vertretbarem Resourcenaufwand finden können. Darauf aufbauend lassen sich anspruchsvollere mathematische Sätze interaktiv formal beweisen, indem eine "Formalisierung" in Form von Zwischenschritten eingegeben wird, die sukzessive von einem automatischen Beweiser verifiziert werden.

In dem Seminar werden wir Techniken des automatischen und interaktiven Beweisens anhand des Handbook of Practical Logic and Automated Reasoning von John Harrison studieren und das interaktive Beweissystem Naproche vorstellen. Einige theoretische Resultate werden aus dem Bonner Logik-Skript übernommen. Programme können u.a. von der Homepage von John Harrison heruntergeladen werden. Die Teilnehmer/innen sollen diese auf ihren eigenen Laptops laufen lassen und kleinere Übungsaufgaben lösen. Die Laptops sollten stark genug für die Beweiserplattform Isabelle sein, die auch das System Naproche enthält.

Vortragseinteilung:

  1. 12.10., Nora Depenheuer: OCaml made light of: Harrison 603-616
  2. 19.10., Ludwig Monnerjahn: Symbols, words, expressions: Koepke 5-8/ H 13-22
  3. 26.10., Simon Walerus: Formulas and syntactic operations, tautologies: H 30-36, 40-48
  4. 2.11., Lars Nießen: Normal forms: K 38-40, H 49-61
  5. 9.11., Hannah Scholz: Davis Putnam procedure: H Subsection 2.9
  6. 16.11., Johannes Folltmann: First-order normal forms, Herbrand's theorem: K 40-43
  7. 23.11., Simon Korswird: Syntax of first-order logic: H 3.1, 3.2, 3.4-3.6
  8. 30.11., Daniel Podstavek: Mechanizing Herbrand's theorem: K 51-53, H 3.8
  9. 7.12., Juliana Brinker: Unification: K 55-57, H 3.9
  10. 14.12., Joshua Wirtz: Resolution: K 53-54, H 3.11
  11. 21.12., Pascal Herbrich: Tableaux: H 3.10
Last changed: 22 June 2023 pk