Recommended AISE Talks and Activities in Winter 2022/23

Wed 25.1., 14:30 (s.t.) to 15:25, Room WE5/04.004

Prof. Dr. Alexander Steen (Uni Greifswald)

A standard translation for higher-order modal logics

Abstract: Standard translations are a common tool for encoding modal logic formulas into classical logic in a truth-preserving way. Common standard translations include the mapping of propositional modal logic into unsorted first-order logic, and the mapping of first-order modal logic into many-sorted first-order logic. In contrast, encodings into higher-order logic (HOL) offer more flexibility and expressivity. In my talk, I will present ongoing work for a novel translation of higher-order (multi-)modal logics into HOL that supports both rigid and flexible constant/function symbols, different quantification semantics, local and global hypotheses. This work extends and partly simplifies previous work on semantic embeddings. A preliminary evaluation is presented.

Wed 25.1., 15:30 (s.t.) to 16:30, Room WE5/04.004

Dr. Serge Autexier (Director of the Bremen Ambient Assisted Living Lab, DFKI Bremen)

Security and Privacy by Design in the development of multi-center-based machine learning for personalized health and care: some best practices and practical challenges 

Abstract: Security and privacy are of utmost importance for systems processing personal health data. The talk presents the impact of security and privacy requirements on the research and development of a platform to train machine learning models on real patient data from multiple sources in a multi-centre setting. It discusses how they affect the design of the system architecture, the choice of methods as well as the whole the whole research and development process itself. The presentation is based on experiences from two European research projects concerned with developing machine learning based personalized risk predictions for cancer patients and COPD patients and sheds a light on the peculiarities of the used data, the target variables to predict and the mechanisms based on predictive models to support medical personnel.


Wednesday, December 25 (17:00-19:00): Guest presentation in the AISE Master-/Oberseminar by 

Matteo Acclavio (Università Roma Tre): A Graphical Proof Theory for "happens-before"

Abstract: The "happens-before" is an order relation over events playing a crucial role in formal verification. 
Logics modelling this relation by means of a non-commutative connective have been introduced in the literature. 
However, their expressiveness is limited to series-parallel orders. In this talk, after recalling the proof theoretical results for these logics and their connections to process calculi, I will present proof systems operating on graphs instead of formulas. This innovative framework allows us to overcome the restrictions of in-line formulas and to handle non-series parallel orders.

Wednesday, October 26 (17:00-19:00): Guest presentation in the AISE Master-/Oberseminar by 

Lavanya Singh (Palantir, Harvard University): Automated Kantian Ethics: A Faithful Implementation

Lavanya has a background in philosophy and computer science and she has successfully employed the LogiKEy technology (as developed in the AISE group of U Bamberg and the ICR team at U Luxembourg) in her thesis work. At the German national KI'2022 conference she received the best paper award for her contribution with the above title. 

Participation is possible in presence in room WE5/03.004 and online at (Meeting ID: 662 9197 0381, Passcode: AISE-OS-22)

Recommended AISE Talks and Activities in Summer 2022

Tutorial & Workshop on Computational Metaphysics and Intensionality

A tutorial and workshop on computational metaphysics and intensionality was organised on Tuesday, May 31 and Wednesday, June 1. The schedule was as follows:

(Note: Unfortunately Prof. Peter Fritz had to cancel his visit on short notice; hence, the schedule has been revised).

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

Room: WE5/01.006, 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/04.003, 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 — 14:45: 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. 

14:45 — 15:30: Edward N. Zalta & Uri Nodelman (Senior Research Engineer, Stanford University)

   Number Theory Without Mathematics

Abstract: We show that in object theory, no mathematical primitives or axioms are required to derive 2nd-order Peano Arithmetic (PA2) or to prove the existence of an infinite cardinal and an infinite class. In research conducted the past year, we've taken advantage of an object-theoretic theorem by Daniel Kirchner to redefine and recast our Frege-style number theory so that "discernible" objects (whether abstract or ordinary) can be counted. This leads to: (a) a derivation of the Dedekind-Peano axioms following Frege’s plan, but adjusted for a modal setting, (b) a Recursion Theorem, (c) a definition of the primitive recursive functions as relations, (d) a definition of addition and multiplication (which yields the recursive axioms for addition and multiplication as theorems), (d) a derivation of Comprehension for Properties of Numbers, (e) a proof that aleph_0 exists (as the number of the property: being a number), and (f) a proof that the *extension* of the property of being a number is an infinite class.


Session 2:

16:00 — 16:10: Christoph Benzmüller  

Foreword on Universal Logical Reasoning and the LogiKEY Methodology, Infrstructure and Tool Support

16:10 — 16:40: 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.

16:40 — 17:10: 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:10 — 17:30: 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.

 17:30 — 17:50: Michael Mendler (Universität Bamberg)

The Došen Square under construction: A tale of four modalities

Abstract: In classical modal logic, necessity []A, possibility <>A, impossibility []~A and non-necessity <>~A form a Square of Oppositions (SO) whose corners are interdefinable using classical negation. The relationship between these modalities in intuitionistic modal logic is a more delicate matter since negation is weaker. Intuitionistic non-necessity [~] and impossibility <~>, first investigated by Došen, have received less attention and — together with their positive counterparts [] and <> — form a square we call the Došen Square. Unfortunately, the core property of constructive logic, the Disjunction Property (DP), fails when the modalities are combined and, interpreted in birelational Kripke structures à la Došen, the Square partially collapses. We introduce the constructive logic CKD, whose four semantically independent modalities [], <>, [~], <~> prevent the Došen Square from collapsing under the effect of intuitionistic negation while preserving DP. The model theory of CKD involves a constructive Kripke frame interpretation of the modalities. A Hilbert deduction system and an equivalent cut-free sequent calculus are presented. Soundness, completeness and finite model property are proven, implying that CKD is decidable. The logics HK[~], HK[], HK<> and HK<~> of Došen and other known theories of intuitionistic modalities are syntactic fragments or axiomatic extensions of CKD.

(This is joint work with Luke Burke and Stephan Scheele.)


Evening: Informal get together in town