Aleks Knoks. Defeasible Logics with Applications to Normative Systems and Philosophy

The course will provide participants with a solid understanding of some contemporary approaches to defeasible reasoning, including default logic, argumentation theories, and input/output logics. In addition, it will discuss applications of these formal tools to normative systems and some heatedly debated issues in epistemology and ethics. So the course participants will learn how defeasible logics work, as well as how to apply them in the context of normative systems and philosophy.

Eric Pacuit. Logics for Social Choice Theory

There is a long tradition of fruitful interaction between logic and social choice theory. Many different logical systems have been developed that can formalize results in social choice theory. In recent years, much of the research on logic and social choice has focused on computer-aided methods such as SAT solving and interactive theorem proving. This course will be a broad overview of recent work on logic and social choice theory. The course will start by introducing key results in social choice theory (e.g., May's Theorem, Arrow's Theorem, the Gibbard-Satterthwaite Theorem) and the different logical systems that have been developed to formalize these results. The second part of the course will show how SAT solvers have been used to discover new results in the study of voting methods. Finally, the last part of the course will be a brief introduction to the Lean interactive proof assistant and how to use Lean to formalize results in social choice theory.

Michael Benedikt and Jerzy Marcinkowski. The Logic of Views

This introductory course for the logic and computation track will cover logical aspects of views. A view is a selection of information from a dataset, usually described within some logic.

We will deal with some natural questions about the information content of views:

-- when does a view have as much information as another?

-- when does a view have sufficient information to answer a given information need?

-- when does a view keep another piece of information private?

Thomas Icard and Krzysztof Mierzewski. Logic & Probability

In this course we propose to present and discuss some of the most important ideas and results covering various contacts between logic and probability. Topics include qualitative and comparative probability, probability logics and probabilistic logics, non-monotonic reasoning and acceptance rules, logical foundations of probabilistic programming, and zero-one laws in logic. Applications to core ESSLLI areas (computer science, linguistics, philosophical logic) will be emphasized.

Phokion Kolaitis and Andreas Pieris. When Semantics Meets Syntax

The study of model theory typically proceeds from syntax to semantics, that is, the syntax of a logical formalism is introduced first and then the properties of the mathematical structures that satisfy sentences of that formalism at hand are explored. There is, however, a mature and growing body of research in the reverse direction, i.e., from semantics to syntax. Here, the starting point is a collection of model-theoretic or structural properties and the goal is to determine whether or not these properties characterize some logical formalism. The main aim of this course is to present a comprehensive overview of model-theoretic and structural characterizations of first-order logic and of fragments of first-order logic that are encountered in database theory, artificial intelligence, and other areas.

Sonia Marin and Lutz Straßburger. From Axioms to Rules: The Factory of Modal Proof Systems

Modal logics have many applications in computer science and linguistics. There are many different kinds of modal logics determined by the postulated axioms. Recent advances in proof theoretical research has uncovered various ways of designing sound and complete proof systems for modal logics, in such a way that the axioms can be directly translated into proof rules.

The goal of this course is to make the student acquainted with these methods. The level of the course is intended to be introductory. We will introduce the various proof calculi, sequent calculus, labelled sequent calculus and nested sequent calculus. We will also introduce the concept of focusing, and show how it can be used for the construction of efficient proof systems for various modal logics.

Alessandra Mileo. Introduction to Answer Set Programming, extensions and applications

This course will provide an introduction to Answer Set Programming (ASP), a paradigm for declarative problem solving based on the stable model semantics of Logic Programming.

The success of ASP for Knowledge Representation and Reasoning, and the presence of a growing research community around it is due to the availability of efficient answer set solvers, the main ones being CLASP and DLV.

The expressive power of ASP rules goes beyond propositional clauses and as a result a growing number of applications of ASP has emerged in recent years.

Numerous extensions of ASP have been proposed since its first formulation in the early 90s, including but not limited to preferential reasoning, reasoning in dynamic environment and probabilistic logic reasoning.

This course will cover the basics of ASP theoretical background as well as some of its key extensions, applications and tools.

Hans van Ditmarsch and Malvin Gattinger. Knowledge and Gossip

Gossip protocols facilitate peer-to-peer information sharing in possibly partial networks of agents. Each agent starts with some private information and the goal is to share this information among all agents. In distributed gossip protocols, there is no central processor or controller deciding who may call whom, but this is determined by independent pro-active agents and chance. In epistemic gossip protocols, knowledge conditions may restrict possible calls, for example you may not wish to call an agent who you know already to know your secret. In dynamic gossip, agents also exchange 'telephone numbers', which leads to network expansion.

This course gives a survey of results and methods in distributed epistemic gossip. Topics include constructing and revising gossip graphs, exhaustively enumerating call sequences, and model checking the conditions of protocols in suitable logics. We will present both the theory and Haskell-based implementations.

Shay Logan and Andrew Tedder. Canonical Models in First-Order Nonclassical Logics: Advanced Topics

We survey methods for proving completeness for first-order relevant logics, including those for classes of models defined by Kit Fine, on the one hand, and by Edwin Mares and Robert Goldblatt on the other. We contrast these methods, and discuss the philosophical upshots of the various model structures, and consider some extensions, such as to identity. We will also discuss a selection of open problems in the area, and seek to equip students with the expertise to engage with these and related issues.

Stepan Kuznetsov. Complexity of Reasoning in Kleene and Action Algebras

Iteration, or Kleene star, is one of the most mysterious algebraic operations that appears in computer science. Even simple theories involving this operation happen to enjoy properties which are more usual for strong systems with induction (like first-order arithmetic), and thus, high algorithmic complexity. In the proposed course, we survey complexity results for theories of algebras with the Kleene star. We start with classical results by Kozen (1994, 2002) on complexity of equational and Horn theories for Kleene algebras (but with modern proofs, which utilize circular proof systems by Das and Pous), and then head to recent results on action algebras, that is, Kleene algebras with residuals, by Buszkowski and Palka (2007) and the author (2019--2020). A highlight of this course is the usage of Kleene algebra for modelling infinite computations, dual to subexponential modalities in linear logic.

Luca Reggio and Tomáš Jakl. Relating Structure to Power: An Invitation to Game Comonads

There is a remarkable divide in the field of Logic in Computer Science between two distinct strands: one focusing on compositionality and semantics ("Structure"), and the other on expressiveness and complexity ("Power"). It is remarkable because these two fundamental aspects are investigated using almost disjoint methods by almost disjoint research communities.

This course will introduce the exciting and emerging theory of game comonads, recently put forward by Abramsky, Dawar, and their collaborators. Game comonads offer a novel approach to relating categorical semantics, which exemplifies Structure, to finite model theory, which exemplifies Power. We will develop their basic theory and illustrate how they provide a structural and intrinsic account of several concrete notions that play a central role in finite model theory. These range from equivalences with respect to logic fragments (e.g., finite-variable, bounded quantifier-rank, and bounded modal-depth fragments), to combinatorial parameters of structures (e.g., tree-width, tree-depth, and synchronization-tree depth), and model comparison games (e.g., pebble, Ehrenfeucht-Fraissé, and bisimulation games).

Mohan Sridharan. Explainability in Integrated Cognitive Systems Combining Logic-based Reasoning and Data-driven Learning

This advanced course seeks to bring participants to the state of the art in explainable reasoning and learning in integrated cognitive systems that use a combination of knowledge-based reasoning and data-driven learning for automated decision-making. In particular, we will explore the class of such systems that sense and interact with the physical world, use non-monotonic logic to reason with incomplete commonsense domain knowledge, and use machine/deep learning methods to learn from experience. We will discuss how the interplay between representation, reasoning, and learning can be exploited in these systems for reliable decision-making, and to provide relational descriptions as explanations of decisions and beliefs. All related concepts will be illustrated using simple examples drawn from computer vision and robotics, with software agents and physical robots assisting humans in dynamic domains.

Ivan Varzinczak and Iliana M. Petrova. Defeasible Reasoning for Ontologies

This course aims at providing an introduction to reasoning defeasibly over description logic ontologies in the context of knowledge representation and reasoning in AI. Description Logics (DLs) are a family of logic-based knowledge representation formalisms with appealing computational properties and a variety of applications.

The different DLs proposed in the literature provide a wide choice of constructors in the object language. However, these are intended to represent only classical, monotonic knowledge, and are therefore unable to express the different aspects of uncertainty and vagueness that often show up in everyday life such as typicality and exceptions.

The goal of this course is two-fold: (i) to provide an overview of the development of non-monotonic approaches to DLs from the past 25 years, pointing out the difficulties that arise when naively transposing the traditional propositional approaches to the DL case, and (ii) present the latest results in the area.