193
Compulsory

When a course instance has been created from a template, the course instance will be in this state

  • Data is usually still incomplete and everything can still be edited.
  • Lecturers or secretaries can move the state forward to Edited.

Die Vorlesung Logik gibt eine Einführung in Themen der Logik sowie ihrer praktischen Anwendungen. Sie richtet sich primär an Studierende der Mathematik, der Informatik, und Interessierte mit mathematischen Grundlagenwissen.

 

In der Vorlesung behandelt werden Grundlagen der formalen Logik:

  • Aussagenlogik: „dieser Pinguin ist schwarz-weiß“
  • Prädikatenlogik erster Stufe: „und alle Pinguine sind schwarz-weiß, aber nicht alles, was schwarz-weiß ist, ist ein Pinguin“
  • Logik höherer Stufe: „jedoch sind alle Nachfahren von diesem Pinguin schwarz-weiß“
  • Automaten und Turingmaschinen: „das kann man in polynomieller Zeit nachrechnen.“

 

mit theoretischen Schwerpunkten auf:

  • Modelltheorie und Kalküle: Wie formalisiert man logische Schlussfolgerung? Beweise? „Wahrheit“?
  • Beweistheorie und (Un-)Vollständigkeit: Ist alles Schlussfolgerbare wahr, und alles Wahre schlussfolgerbar?
  • Berechenbarkeit und Entscheidbarkeit: … durch einen (Computer-)Algorithmus?

 

Praktische Aspekte stellen einen zentralen Bestandteil der Vorlesung und v.a. der Übungen dar, behandelt werden:

  • Logik und Wissenschaftstheorie: wie axiomatisiert man empirische Beobachtungen? Wann ist eine logische Schlussfolgerung empirisch korrekt? Wie erkennt man mathematisch „korrekte“, aber empirisch unnütze (mathematisch/axiomatische) Modelle oder Schlussfolgerungen? Beispiele und Vermeidung von „Mathematistry“-Pseudowissenschaft.
  • Inferenz- und Beweissysteme: wie formalisiert man logische Schlussfolgerung in einem Computer? Wie überprüft man in-silico, ob eine Schlussfolgerung, ein Beweis korrekt ist? Wie automatisiert man logisches Schlussfolgern im Computer? Der berühmte, vor kurzem erbrachte Maschinenbeweis der Kepler-Vermutung wird hier ausführlich als ein Beispiel-Highlight diskutiert werden.
  • Anwendungen formaler Logik in der technischen Informatik: Schaltkreisdesign, formale Verifikation von Prozessoren.
  • (falls zum Schluss noch Zeit ist und Interesse besteht) eine Einführung in Quantenlogik und Quantencomputing.

This lecture course combines

  • A) a compact introduction in the theory of first-order logic with
  • B) a hands-on tutorial on the development and eployment of first-order theorem proving systems.

Regarding A) the lecture focuses on the textbook of Fitting:  First-Order Logic and Automated Theorem Proving, 1996. Harrison' Handbook of Practical Logic and Automated Reasoning, 2009, is also recommended. The topics of this part of the lecture include:

  • syntax and semantik of propositional logic and first-order logic (with and without equality);
  • Herbrand models;
  • Hintikka sets and abstract consistency;
  • soundness and completeness;
  • semantic tableaux and Resolution;
  • implementation 

 

 

Regarding B) the lecture focuses on the TPTP infrastruktur (www.tptp.org). Addressed topics include:

 

  • TPTP Sprache(n)
  • SZS ontology of prover results
  • TPTP and TSTP libraries for problems and proofs
  • application and developement of TPTP compliant provers 
  • further TPTP tools and systems
  • TPTP infrastructure for higher-order logic

Part B) of the lecture we will predominantly work practically.  As far as time permits we will also address selected topics on the theory and practice of higher-order automated theorem proving. Students are advised to start reading the suggested literature before the lecture course starts.

Cross-language

193 242
Compulsory

Expectant Mother

Not dangerous
Partly dangerous
Alternative Course
Dangerous

Nursing Mother

Not dangerous
Partly dangerous
Alternative Course
Dangerous

AncillaryCourses

Übung zu Logik

Expectant Mother

Not dangerous
Partly dangerous
Alternative Course
Dangerous

Nursing Mother

Not dangerous
Partly dangerous
Alternative Course
Dangerous