Expressive Klassische und Nichtklassische Logiken und deren Automatisierung
--- Seminar Winter 2013/14 ---
Seminar (Nr. 19675) - 2-stündig, ECTS: 4
Dozenten:
Christoph
Benzmüller
Ort: SR 140/A7 Seminarraum (Hinterhaus)
Termine: siehe unten
Zielgruppe: Studenten mit Interesse an Logic und Deduktionssystemen
Voraussetzungen: Studenten ab dem 5. Semester, Grundkenntnisse und Logik und theoretischer Informatik
Maximale Anzahl von Teilnehmern: 15
Website: http://christoph-benzmueller.de/2013-ExLog/
Inhalt
Im Fokus dieses Seminars stehen ausdrucksstarke klassische und nichtklassische Logiken, beispielsweise: Klassische Logik höherer Stufe, Quantifizierte Modallogiken (einschliesslich Temporallogiken), Quantifizierte Konditionale Logiken, Quantifizierte Mehrwertige Logiken, usw.
Diese Logiken sind von grossem Interesse für die Informatik, die Künstliche Intelligenz, die Philosophie und die Computerlinguistik. Ihre Automatisierbarkeit ist allerdings als sehr schwierig einzustufen, was praktische Anwendungen bisher weitgehend ausschloss.
Wir werden die Theorie einiger solcher expressiven Logiken skizzieren und aktuelle Fortschritte hinsichtlich ihrer Mechanisierung und Automatisierung diskutieren.
Es ist geplant, dass in diesem Seminar auch verschiedene externe
Wissenschaftler Vorträge anbieten.
Vorbesprechung
Eine erste Vorbesprechung fand am Freitag, dem 12. Juli 2013, um 14:00 Uhr statt.
Eine zweite Vorbesprechung findet am Freitag, dem 11. Oktober 2013, um 14:00 Uhr; SR 140/A7 Seminarraum (Hinterhaus).
Einarbeitung
Alle Teilnehmer des Seminars sollten folgenden Artikel gründlich
durchlesen:
Jeder Teilnehmer erhält dann ein eigenes Vortragsthema zugewiesen, verbunden
mit der Durcharbeitung mind. eines weiteren Artikels.
Termine (diese Angaben sind vorläufig)
- Fr 11.10.2013 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Finale Vorbesprechung (Benzmüller)
- Einführung in das Thema (Benzmüller)
- Fr 18.10.2013 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Klassische Logik höherer Stufe (Church's Type Theory, HOL) I -- Motivation, Syntax und Semantik (Ziener)
- Andrews, Peter, Church's Type Theory, The Stanford Encyclopedia of Philosophy (Spring 2009 Edition), Edward N. Zalta (ed.)
- Andrews, P., 2001, Classical Type Theory, in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Volume 2/Chapter 15, Amsterdam: Elsevier Science, pp. 965-1007.
- Fr 25.10.2013 14:00 - 16:00 Takustr. 9, SR049 - Kaffee ab 13:45 Uhr im Konferenzraum 137
- Isabelle/HOL- Interaction and Automation (Vortrag von J. Blanchette im Informatik Kolloquium; siehe auch Ankündigung im CMS)
- Fr 01.11.2013 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Formalization, Mechanization and Automation of Gödel's Proof of God's Existence (Vortrag von C. Benzmüller und B. Woltzenlogel-Paleo und ; siehe auch Ankündigung im CMS)
- Fr 08.11.2013 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Logik erster Stufe, Logik Zweiter Stufe, Logik höherer Stufe (Furmanczuk)
- Enderton, Herbert B., Second-order and Higher-order Logic, The Stanford Encyclopedia of Philosophy (Fall 2012 Edition), Edward N. Zalta (ed.)
- Boolos, George, 1975. On Second-Order Logic, The Journal of Philosophy, 72:509-527. Also in Logic, Logic, and Logic, by George Boolos, Cambridge, MA: Harvard University Press, 1998, pp. 37-53.
- Leivant, Daniel, Higher Order Logic, Handbook of Logic in Artificial Intelligence and Logic Programming (2) 1994: 229-322
- Fr 15.11.2013 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Nichtklassische Logiken vs. Klassische Logiken (Weber)
- Burgess, John P., Philosophical logic, Princeton University, 2009
- Fr 22.11.2013 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Modallogiken I --- Motivation, Syntax und Semantik (Wisniewski)
- Garson, James, Modal Logic, The Stanford Encyclopedia of Philosophy (Spring 2013 Edition), Edward N. Zalta (ed.)
- Popkorn, S., 1995, First Steps in Modal Logic, Cambridge: Cambridge University Press.
- Chellas, B., 1980, Modal Logic: An Introduction, Cambridge: Cambridge University Press.
- Fr 29.11.2013 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Modallogiken II --- Automatisierung mit
Spezialbeweisern (Jens Otten, Universitüat Potsdam)
- Fr 06.12.2013 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Modallogiken III --- Automatisierung als HOL Fragmente (Steen)
- Benzmüller, Christoph, Paulson, Lawrence,
Quantified Multimodal Logics in Simple Type Theory, In Logica Universalis (Special Issue on Multimodal Logics), volume 7, number 1, pp. 7-20, 2013.
- Benzmüller, Christoph, Otten, Jens, Raths, Thomas, Implementing and Evaluating Provers for First-order Modal Logics, In Proc. of the 20th European Conference on Artificial Intelligence (ECAI), pp. 163-168, 2012.
- Fr 13.12.2013
- --- kein Seminar ---
- Fr 20.12.2013 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- --- kein Seminar ---
- Fr 10.01.2014 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Demonstration: Beweisen in
Nicht-klassischen Logiken I (Benzmüller)
- Fr 17.01.2014 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Demonstration: Beweisen in
Nicht-klassischen Logiken II (Benzmüller)
- Fr 24.01.2014 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Konditionale Logiken I --- Motivation, Syntax und
Semantik (Scholz)
- Horacio Arlo-Costa, The Logic of Conditionals, The Stanford Encyclopedia of Philosophy (Spring 2013 Edition), Edward N. Zalta (ed.)
- Nute, Donald, Topics in Conditional logic, Philosophical studies series in philosophy, vol. 20.
D. Reidel Publishing Company, Dordrecht, Boston, and London, 1980
- Lewis, David, Counterfactuals, Oxford: Blackwell Publishers and
Cambridge: Harvard University Press, 1973, Reprinted with revisions,
1986.
- Fr 31.01.2014 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Konditionale Logiken II --- Automatisierung als HOL Fragmente (Benzmüller)
- Fr 07.02.2014 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Kombinationen von Logiken und Metalogisches Schliessen in HOL (Benzmüller)
- Fr 14.02.2014 14:00 - 16:00 SR 140/A7 Seminarraum (Hinterhaus)
- Abschlussdiskussion (Benzmüller)
C. Benzmüller, 2013