From Dynamic Epistemic Logic to Socially Intelligent Robots
Abstract: Dynamic Epistemic Logic (DEL) can be used as a formalism for agents to represent the mental states of other agents: their beliefs and knowledge, and potentially even their plans and goals. Hence, the logic can be used as a formalism to give agents a Theory of Mind allowing them to take the perspective of other agents. In my research, I have combined DEL with techniques from automated planning in order to describe a theory of what I call Epistemic Planning: planning where agents explicitly reason about the mental states of others. One of the recurring themes is implicit coordination: how to successfully achieve joint goals in decentralised multi-agent systems without prior negotiation or coordination. The talk will first motivate the importance of Theory of Mind reasoning to achieve efficient agent interaction and coordination, will then give a brief introduction to epistemic planning based on DEL, address its (computational) complexity, address issues of implicit coordination and, finally, demonstrate applications of epistemic planning in human-robot collaboration.
About: Thomas Bolander, PhD, is a professor of logic and artificial intelligence (AI) at DTU Compute, Technical University of Denmark. His main research focus is on the modelling of social phenomena and social intelligence with the aim of creating explainable AI systems that can interact robustly and intelligently with other agents (humans and AI systems). He is one of the main researchers within the area of Epistemic Planning providing AI agents, e.g. robots, with the ability to take the perspective of other agents into account when planning. He is also one of the central public communicators of AI in Denmark. In 2019 he received the H.C. Ørsted award for excellence in science communication, and in 2024 he received the DAIR Lifetime Achievement in AI award.
Declarative Foundations, from Graph Data to Neurosymbolic AI
Abstract: As data processing becomes increasingly AI-driven, much of the burden of correctness rests on specifications. We examine three aspects of how declarative specifications govern property graph data, drawn from our recent work: validity (which invariants recent property graph constraint languages can express), evolution (reliably refactoring the data's underlying structure without loss of information), and collaboration (concurrent edits converging to a valid state without coordination). We then ask how far these foundations carry into neurosymbolic AI. Focusing on systems with an explicit symbolic core, i.e., logic-based languages such as Datalog, answer-set, and probabilistic logic programs, we present, to our knowledge, the first survey aligning their features with application needs along semantic, expressiveness, neural-integration, and computational axes. We close by revisiting validity, evolution, and collaboration from a neurosymbolic perspective, and outline open directions.
About: Stefania Dumbrava is an Associate Professor at ENSIIE and the SAMOVAR laboratory of Télécom SudParis, currently on leave at INRIA. She earned her PhD from Paris-Saclay University in 2016. Her research lies at the intersection of data management and formal methods, focusing on reliable graph data processing. She is the Principal Investigator of the ANR JCJC project VERDI on verified foundations of distributed graph systems. She is Proceedings Co-Chair of VLDB 2027, Demonstration Track Co-Chair of VLDB 2026, and has co-organized the VLDB Summer School and several graph data management workshops at SIGMOD/PODS, EDBT, and STAF. She serves on the editorial board of the TGDK journal and the review board of ACM TODS. She has received the EASST Best Software Science Paper Award at ICGT 2025, a Research Highlight Award and a Best Industrial Track Paper Award at SIGMOD 2023, and a Best Paper Runner-Up Award at VLDB 2022.
Solving Hard Optimization Problems by (de)coupling Reasoning and Optimization
Abstract: The impact of breakthroughs in practical automated reasoning systems---such as Boolean satisfiability (SAT) solvers and their extensions---goes well beyond "merely" solving NP decision problems declaratively. Among the various success stories are SAT-based approaches to exactly solving NP-hard combinatorial optimization problems. The implicit hitting set approach offers a general, constraint-agnostic framework to constraint optimization based on hitting set duality, on a high level stating that optimal ways of relaxing away all underlying inconsistencies among constraints at hand results in solutions to the remaining non-relaxed constraints being optimal. In practice, IHS solvers iteratively employ various heuristics for using decision procedures to identify “core” constraints over objective variables entailed by the problem constraints at hand, as well as optimizers for discovering ways of relaxing out these sources of inconsistencies. IHS-based optimizers have been successfully instantiated for various declarative paradigms, and, alongside other applications, also captures general notions of explanations. In this talk, I aim to give a high-level overview of the IHS approach and highlight our recent advances in extending IHS to certified, incremental and multi-objective optimization.
About: Matti Järvisalo is Professor of Computer Science (Algorithms and Machine Learning) at University of Helsinki, Finland, where he leads the Constraint Reasoning and Optimization group. His research interests span several areas in artificial intelligence, including automated reasoning and declarative programming, combinatorial optimization, knowledge representation and graphical models, with key contributions especially in theory and practice of Boolean satisfiability (SAT), SAT-based decision, combinatorial optimization and counting procedures, and their applications. His group has been successful in developing state-of-the-art solvers and tools e.g. for SAT, maximum satisfiability (MaxSAT), pseudo-Boolean optimization, formal argumentation, and answer set programming. With over 160 peer-reviewed publications to date, Dr. Järvisalo has received various best paper awards and other international recognitions for his contributions, including the IJCAI-JAIR Best Paper Award and an IJCAI Early Career Spotlight, as well as further best paper recognitions at ECAI, CP, KR, ICLP and PGM. In addition to organizing various workshops and conferences, he was PC Chair for SAT'13, IJCAI-PRICAI'20 Demo Track, KR'23 Applications and Systems Track, and KR'24 In the Wild Track, Chair of the Finnish AI Society (EurAI member society of Finland) 2019-2021, and has served on program committees of over 100 conferences. Today he serves on the editorial boards of Journal of Artificial Intelligence Research, Journal of Automated Reasoning, and Journal of Satisfiability, Boolean Modeling and Computation. Dr. Järvisalo has also been involved in organizing various automated reasoning competitions, including the renown SAT solver competitions and MaxSAT Evaluations for many years.