Das wird heiß

— Makarius

Programm für das einundzwanzigste Treffen am 1. Dezember 2016

Gepostet am 6. Nov 16 von Tim Baumann

Makarius gibt eine Einführung in die Grundlagen von klassischer Logik höherer Ordnung mit Hilberts Auswahloperator.

  • History of Higher-Order Logic
  • Implementations of HOL
  • Quasi-programming in Isabelle/HOL
  • Isabelle foundations: primitive inferences, object-logic rules, rule composition, structured proofs Foundations of Higher-Order Logic: actual Isabelle/HOL, Pure bootstrap of HOL
  • Isabelle theory with some exercises (for Isabelle2016-1)

Anschließend leitet Profpatsch eine gemeinsame Programmiersitzung an.