A tutorial and workshop on computational metaphysics and intensionality is organised (as part of the Oberseminar of the AISE group) on Tuesday, May 31 and Wednesday, June 1. The schedule is as follows:

Tuesday, May 31: Tutorial 14:00 - 18:00

Room: WE5/05.1006, An der Weberei 5, 96047 Bamberg

Tutorial: Using Isabelle/HOL in Computational Metaphysics (by Daniel Kirchner, Edward N. Zalta, Christoph Benzmüller)

Wednesday, June 1: Workshop 13:45 - 18:00

Room: WE5/05.4003, An der Weberei 5, 96047 Bamberg

Session 1: 

13:45 — 14:00: Christoph Benzmüller (Professor for AI Systems Engineering, University of Bamberg & FU Berlin)

Welcome

Brief Introduction to the AISE Research Group at the University of Bamberg

14:00 — 15:00: Edward N. Zalta (Senior Research Scholar, Philosophy Department, Stanford University)

Resolving Ambiguities in the Data: How to Connect Logic and Deep Learning Methodologies

Abstract: In this talk, I attempt to build a bridge between computer scientists who use deep learning techniques and logicians who develop formal representations.  My test case will be understanding, explanation, and reasoning in mathematics, namely, how to reconcile formal logical analyses and deep learning analyses of these phenomena.  I'll explore some common ground and then highlight some key ambiguities in the data that are resolved by a logical system with two kinds of predication. This has implications for designing and training deep-learning systems for understanding mathematical language -- there are unmarked structural and lexical ambiguities in the training data that, once resolved logically, may lead to better success in building AI systems. 

15:00 — 15:30: Daniel Kirchner (Doctoral Candidate in Mathematics, FU Berlin & Ethereum Foundation)

Applying computational methods to a foundational metaphysical theory.  

Abstract: In this talk, I report on a recent research project in which we effectively implemented a custom theorem proving environment for a foundational metaphysical theory by means of a shallow semantic embedding in classical higher-order logic. I discuss how existing infrastructure for automated and interactive reasoning could be transferred to a theory that is based on fundamentally different logical primitives compared to the meta-logic and how this process could lead to significant advances in the targeted theory.

Coffee Break

Session 2:

16:00 — 17:00: Peter Fritz (Professor for Philosophy, Australian Catholic University, Melbourne, Australia)

Higher-Order Logic and the Individuation of Propositions  

Abstract: I consider the individuation of propositions in the context of higher-order logic. It may seem that propositional attitudes like knowledge require propositions to be very finely individuated. For example, since someone might know that 2+2=4 without knowing that there are infinitely many primes, it may seem that these two propositions must be distinct. I argue that once we adopt a higher-order formalization of talk of propositions, we cannot rely on such direct arguments for the distinctness of propositions using propositional attitudes. Nevertheless, I argue that propositional attitudes can be used to argue for a limited amount of fineness of grain of propositions.

17:00 — 17:30: Luke Burke (Postdoctoral Researcher in Theoretical Computer Science, University of Bamberg)

Dynamic approaches to Logical Omniscience and natural language semantics

Abstract: Much work in epistemic logic aims to avoid the strong closure conditions on knowledge and belief modalities  which engender the problem of Logical Omniscience. Some recent approaches to the problem of Logical Omniscience aim to capture the way that agents apply deductive rules, in a stepwise and cumulative manner, unravelling the logical consequences of what they believe bit by bit. Such approaches use the resources of dynamic epistemic modal logic, in which the action of an agent deducing a consequence is captured by a modal operator which shifts the model at which a formula is evaluated. So far such approaches have been elaborated mainly within the context of modal propositional logic. But from the vantage point of natural language semantics, such a setting is not rich enough; in fact, a higher-order setting is preferable, since we need to be able to capture the contribution of determiners such as every and some, which usually treated as functionals. In this talk we elaborate an approach to logical omniscience which incorporates a mechanism accounting for stepwise reasoning process into the simply-typed lambda calculus, the engine of much work in compositional natural language theory. Our account leads to an interesting view on meaning as related to chains of deductive inference. 

17:30 — 18:00: David Fuenmayor (Doctoral Candidate in Computer Science, FU Berlin & University of Luxemburg & University of Bamberg)

On using mathematical proof assistants for logico-philosophical investigations

Abstract: I discuss how modern mathematical proof assistants based upon Church's simple theory of types (aka. HOL) can be harnessed to allow logical reasoning with modal and other non-classical systems (paraconsistent, paracomplete, substructural, etc.). Previous work on computational philosophy by employing this approach is surveyed and some prospective applications for computational metaphysics are outlined.

Evening: Informal get together in town