AISE-UL: Universelle Logik und Universelles Schließen
Knowledge representation and reasoning applications in computer science, AI, philosophy and math typically employ very different logic formalisms. Instead of a "single logic that serves it all" (as envisioned already by Leibniz) an entire "logic zoo" has been developed, in particular, during the last century. Logics in this zoo, e.g., include modal logics, conditional logics, deontic logics, multi-valued logics, temporal logics, dynamic logics, hybrid logics, etc. In this lecture course we will introduce, discuss and apply a metalogical approach to universal logical reasoning that addresses this logical pluralism. The core messageis this: While it might not be possible to come up with a universal object logic as envisioned by Leibniz, it might in fact be possible to have a universal meta logic in which we can semantically model, analyse and
apply various species from the logic zoo. Classical higher order logic (HOL) appears particularly suited to serve as such a universal meta logic, and existing reasoning tools for HOL can fruitfully be reused and applied in this context.
Lernziele/Kompetenzen:
The participants of this course will, in combination with a hands-on introduction to Isabelle/HOL, learn about HOL, about semantical embeddings (SSE technique) of non-classical logics in HOL, and about proof automation of these logics in Isabelle/HOL. They will conduct practical exercises regarding the application of the SSE technique in philosophy, mathematics or artificial intelligence, including, normative reasoning and machine ethics.
Empfohlene Vorkenntnisse: Basic knowledge about classical and non-classical logics, theoretical computer science
Knowledge representation and reasoning applications in computer science, AI, philosophy and math typically employ very different logic formalisms. Instead of a "single logic that serves it all" (as envisioned already by Leibniz) an entire "logic zoo" has been developed, in particular, during the last century. Logics in this zoo, e.g., include modal logics, conditional logics, deontic logics, multi-valued logics, temporal logics, dynamic logics, hybrid logics, etc. In this lecture course we will introduce, discuss and apply a metalogical approach to universal logical reasoning that addresses this logical pluralism. The core messageis this: While it might not be possible to come up with a universal object logic as envisioned by Leibniz, it might in fact be possible to have a universal meta logic in which we can semantically model, analyse and
apply various species from the logic zoo. Classical higher order logic (HOL) appears particularly suited to serve as such a universal meta logic, and existing reasoning tools for HOL can fruitfully be reused and applied in this context.
Lernziele/Kompetenzen:
The participants of this course will, in combination with a hands-on introduction to Isabelle/HOL, learn about HOL, about semantical embeddings (SSE technique) of non-classical logics in HOL, and about proof automation of these logics in Isabelle/HOL. They will conduct practical exercises regarding the application of the SSE technique in philosophy, mathematics or artificial intelligence, including, normative reasoning and machine ethics.
Empfohlene Vorkenntnisse: Basic knowledge about classical and non-classical logics, theoretical computer science
- Moderator/in: Christoph Benzmüller
- Moderator/in: David Fuenmayor Pelaez
Semester: 2024/25 Wintersemester