Universal Logical Reasoning
Christoph
Benzmüller
Lecture Course and Exercises, Dep. of Mathematics and
Computer Science, Freie Universität Berlin
Winter 2018/19
Date and Place:
Lecture: Tuesdays, 10:15-11:45, T9/053 Seminarraum (Takustr. 9)
Exercises: Tuesdays, 12:30-14:00, T9/053 Seminarraum (Takustr. 9)
Core Reading Material (to be extended):
Universal
(Meta-)Logical Reasoning: Recent Successes
Church's
Type Theory
Quantified Multimodal Logics in Simple Type Theory
A Deontic Logic Reasoning Infrastructure
A
Dyadic Deontic Logic in HOL
Higher-Order Modal Logics: Automation and Applications
Further Reading Material (to be extended):
Isabelle/HOL Tutorials
Automating Free Logic in HOL, with an Experimental Application
in Category Theory
Mechanizing Principia
Logico-Metaphysica in Functional Type Theory
Automation of
Higher-Order Logic
Higher-Order
Semantics and Extensionality
The Seven Virtues of Simple Type Theory
Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure
The Lambda Calculus
Lambda Calculi with Types
Systematic
Verification of the Modal Logic Cube in Isabelle/HOL
Handbook of Deontic Logic and Normative Systems
Handbook
of Legal Reasoning and Argumentation
Constructing
argument graphs with deductive arguments: a tutorial
Fuzzy
Modal Logic
Automating Free Logic in HOL, with an Experimental Application in Category Theory
Axiom Systems for Category Theory in Free Logic
Examples of Formalisation Sources (to be extended) :
Example.thy:
Some introductory examples
Hilbert
calculus in Isabelle/HOL
Wise Men Example (from paper: Universal
(Meta-)Logical Reasoning: Recent Successes)
Category Theory Examples (from paper: Automating Free Logic in HOL, with an Experimental Application
in Category Theory)
GDPR
Examples (Deontic Logic) (from papers: A Deontic Logic Reasoning
Infrastructure and A Dyadic Deontic Logic in HOL)
Various
further examples (from 2017-PUCRS-Tutorial in Porto Allegre)
Further Technical Material :
Short manual on PDF creation in Isabelle (english)
More detailed manual on PDF creation in Isabelle (german)
Miscellaneous (to be continuously extended) :
Youtube
Video related to Introductory Lecture
Slides (1-2) Introductory Lecture
Slides
(3-7) HOL, HOML, Semantical Embedding, etc.
Potential Topics and Reading/Information Material for Formalisation Projects (to be extended) :
Grundgesetz
für die Bundesrepublik Deutschland
StVO
BGB
Ethical
Aspects of Climate Engineering
debatelab@KIT
Wie
argumentieren Rechtspopulisten (Lanius)
Wahlprogramme 2017 der Parteien: AfD
Bündnis 90 / Die Grüne, CDU/CSU,
FDP,
Linke,
SPD, Tweets by politicians, etc.
Brexit Agreement and Debate:
EU Draft Agreement, British Documents
Exercises (to be extended) :
1. Install Isabelle/HOL; read in the tutorials; play with Sledgehammer and Nitpick
2.a. Select and formulate a valid conjecture in
classical first-order logic; prove it
2.b. Select and formulate an invalid conjecture in
classical first-order logic; generate a countermodel with Nitpick and/or
Nunchaku
3.a. Select and formulate a valid conjecture in
classical higher-order logic; prove it
3.b. Select and formulate an invalid conjecture in
classical higher-order logic; generate a countermodel with Nitpick and/or Nunchaku
4. Download the sources for the wise men puzzle example
(see above)
and read the "recent successes" paper (see above) again; do you
understand the modeling and agree with it; eventually consult
secondary literature as mentioned; can you formulate the riddle
also for 2 or 4 wise
men; do the theorem provers and model finders still respond?; do
you have an idea on how the dynamics of the scenario could be
adequately captured (hint: dynamic epistemic logic)
5. Use the example file from exercise 4. and encode and prove the
Sahlqvist correspondences (see page 22 in the slides). Can
you prove some of these correspondences interactively at a fine
grained interaction lavel (in particular without using sledgehammer).
6. Further experiments with the Sahlqvist correspondences
and the modal logic cube are described in this paper. Please
reconstruct these experiments in your environment and play with
them.
7. Exercise on probalistic reasoning proposed by Mateja
Jamnik (Cambridge): See here.
8. Prepare one primary and one secondary topic for
formalisation within the universal (meta-)logical reasoning
approach. Respective topic suggestions have been given
above. Conduct an analysis as suggested in the lecture and start
with prototype formalisations. Be prepared to briefly present your
analysis in the lecture/tutorial on Dec 18.
Group work:
Group 1. (Jonas von der Heyden, Lucca Tiemes, Florian
Dorner, Kai Sauerland): Embedding of Fuzzy Logic in HOL (11.12. +
18.12.)
Group 2. (Janina Hantke, Celina Loeper, Viktoria Sorgalla,
Valeria Zaharansky, Jaume Delclos): Publishing with Isabelle/HOL (6.11.)
Group 3. (Sebastian Reiche, Lutz Schäfer, Adriana
Pinto, Andi Bauer, Alu Nietner): Wise Men Puzzle (13.11.); Project
preference: Climate Change
Group 4. (Cipriano Aranda, Leon Dirmeier, Thomas Harms,
Carmen Johansmeier): Introduction to Argumentation Theory (30.10. +
6.11.), Brexit projetc (8.1.)
Group 5. (Hannah Treppens, Maria Hartmann, Lilli Joppien,
Joao Petrosa): AfD platform on immigration (8.1.)
Group 6. (Claas Fandre, Daniel Sadewasser, Manuel Leppert,
Lars Parmakerli):
C. Benzmüller (Last modified: Tue Jan 15 15:17:53 CET 2019 )