# Courses' slots:

- Week one 9:00 - 10:30
- Week one 11:00 - 12:30
- Week one 14:00 - 15:30
- Week one 17:00 - 18:30
- Week two 9:00 - 10:30
- Week two 11:00 - 12:30
- Week two 14:00 - 15:30
- Week two 17:00 - 18:30

# Week one 9:00 - 10:30

## Logic and Computation foundational course:

Ontology Modelling Languages.

Teachers
Abstract:
Ontologies are currently becoming the major paradigm for knowledge representation and reasoning. Their success is driven by the Semantic Web effort, but there is also considerable use outside the Web context, e.g. in information integration or life sciences. In this course, we will present an in-depth treatment of the ontology representation languages RDF and OWL, which are recommended standards by the World Wide Web consortium. We will thoroughly examine their logical underpinnings and discuss current research topics and applications. The outline of the course will be as follows:

(1) RDF and RDF Schema

(2) OWL and Description Logics

(3) Tableaux algorithms for OWL

(4) Query languages

(5) Applications.

## Logic and Computation introductory course:

Non-deterministic Multi-valued Logics.

Teachers
- Arnon Avron ()
- Beata Konikowska ()

Non-deterministic multi-valued logics is a recent natural generalization of ordinary multi-valued logics which has been inspired by the idea of non-deterministic computation from Computer Science. In this course we introduce the basic concepts and results related to both ordinary multi-valued logics and their non-deterministic generalizations. We then demonstrate the usefulness of the non-deterministic approach by providing semantics for thousands of non-classical logics, in particular paraconsistent logics, fuzzy logics and other logics for reasoning under uncertainty. Another application which will be described is the construction and characterization of analytic proof systems for a variety of logics, including classical and intuitionistic logics (the relevant proof theoretical concepts will be described in the course). Another application which will be dealt with in the course using the tool of non-deterministic logics is a complete mathematical solution to the famous philosophical "Tonk" problem. The course assumes only a basic background in formal logic.

# Week one 11:00 - 12:30

## Logic and Computation introductory course:

Temporal logics for specification and verification.

Teacher
Course material: Goranko-ESSLLI2009CourseNotes.pdf

Abstract:
The course will cover the following topics:

I. Transition systems and computations. Important properties of
transition systems: safety, eventualities, fairness,
reachability. Formal specification and verification of
properties of transition systems. Temporal logics as languages
for specification.

II. Linear and branching time models of computations.

Linear time temporal logics. Expressing properties of
computations in transition systems using LTL.

Satisfiability of LTL specifications. Verification of LTL
specifications by model checking.
Branching-time temporal logics. Expressing properties of
computations in transition systems using CTL and CTL*.

Satisfiability of CTL specifications. Verification of CTL
specifications by model checking.

III. Buchi automata on infinite words and trees. Automata
recognizing models of temporal formulae.

Automata-based methods for satisfiability and model checking of
linear and branching time temporal formulae.

IV. Tableau-based methods for testing satisfiability and
model-checking of linear and branching time temporal formulae.

V. Optional, subject to time availability: Introduction to modal
mu-calculus. Model checking of mu-calculus formulae.

## Logic and Computation introductory course:

Logics of individual and collective intentionality.

Teachers
Abstract:
This course presents basic concepts about individual and
collective intentionality which have been studied in the
multi-agent domain and in the philosophical domain. We will
discuss the most important logical theories developed in the
last two decades to formalize individual and collective
attitudes such as knowledge, belief, preference, intention,
group belief (i.e. distributed belief, common belief, collective
acceptance), collective intention. The course is also devoted to
clarify the philosophical foundations of such concepts. In the
first part of the course we will focus on individual
attitudes. In the second part of the course we will focus on
collective attitudes.

COURSE OUTLINE.

KNOWLEDGE AND BELIEF (Day 1):

- Kripke models, logics S5, KD45;

- Omniscience problem;

- Link between belief and knowledge.

GOALS AND INTENTIONS (Day 2):

- Bratman's theory of intention;

- Cohen & Levesque's logic of intention;

- Other BDI approaches (Rao & Georgeff, Meyer & Van der
Hoek, Wooldridge);

- Intention, intentional actions and attempts.

DYNAMICS OF BELIEFS, GOALS AND PREFERENCES (Day 3):
- Dynamic Epistemic Logic (DEL);

- Belief revision (AGM approach);

- Integrations of DEL and AGM;

- Logics of goal and preference change (Liu, Shapiro et al.).

GROUP BELIEF (Day 4):

- Philosophical theories of group belief (Lewis, Tuomela, Gilbert);

- Logics of distributed, mutual and common belief;

- The logic of collective acceptance.

GROUP INTENTION (Day 5):

- Philosophical theories of collective intention (Bratman, Tuomela);

- Logical theories of collective intention (Cohen et al., Grosz
& Kraus, Dunin-Keplicz & Verbrugge).

PREREQUISITES.
We assume basic background knowledge of modal logic.

# Week one 14:00 - 15:30

## Logic and Computation advanced course:

Game semantics and its applications.

Teacher
Abstract: In recent years game semantics has emerged as a robust paradigm for giving semantics to a variety of logical systems and programming languages. Its precision in modelling has subsequently led to original applications in program analysis and model checking. This course is meant to provide a self-contained introduction to the field along with a survey of ongoing applied work.

## Logic and Computation workshop:

Logical Methods for Social Concepts.

Organizers
Course material: AquilkhanBanerjee.pdf BalbianiDitmarschSeban.pdf Broersen.pdf DegremontKurzen.pdf Dimitri.pdf EckertHerzberg.pdf GenotJacot.pdf GhoshVelazquez.pdf GierasimczukKurzenVelazquez.pdf HakliNegri.pdf LonginNguyen.pdf RousselCholvy.pdf Tuomela.pdf

Abstract:
Both computer science and the social sciences are interested in
concepts such as power, cooperation, responsibility, delegation,
trust, reputation, convention, agreement, commitment, etc. The
aim of the workshop is to study whether logical approaches
developed in the multi-agent system (MAS) domain are adequate to
express them in an accurate way. In particular, are existing
logical approaches sufficiently expressive to capture the main
features of these social concepts? Are the basic assumptions in
the existing logics for MAS too strong to capture the
fundamental aspects of social phenomena? Are some concepts
relevant for social theory missing in these logics?

We encourage not only works focused on the technical aspects of
logics for multi-agent system, but also works including
multidisciplinary aspects from social sciences (e.g. economics,
sociology, social philosophy) and providing a critical analysis
of the existing logical frameworks for the specification of
social concepts. Indeed, the workshop is intended to bring
together logicians and social theorists in order to provide a
better understanding of the potentialities and limitations of
logical methods for the analysis of social reality.

The following are some examples of topics that are relevant for the workshop.

- Logics of individual and collective powers
- Logical approaches to game theory
- Public announcements logics and logics of communication
- Logical approaches to trust and reputation
- Logical approaches to organizational concepts (e.g. roles, responsibility, delegation)
- Logics of social commitment and collective attitudes
(e.g. common belief and common knowledge, collective acceptance,
joint intentions)

- Logics for mechanism design

## Logic and Computation advanced course:

Reasoning in complex theories and applications.

Teacher
Course material: sofronie-lecture-esslli-09.pdf

Abstract:
The goal of this course is to give a comprehensive, in-depth
perspective on recent advances in the field of reasoning in
complex logical theories, and to present the applications of
these results in mathematics, formal verification and knowledge
representation.

We will start by explaining the importance of logical
formalization in various areas (mathematics, verification,
knowledge representation, AI). We will point out the
limitations of the logic formalization, as well as the necessity
of developing decision procedures. We will argue, using various
examples, that concrete problems often are quite heterogeneous
in nature, such that combinations of reasoning tools
(resp. decision procedures) for various theories might be needed
in the same application. We will introduce the necessary
theoretical concepts and give a survey of decidable and
tractable logical theories. We will then present recent
achievements which address the main problems which occur in this
context, starting from SAT checking in classical logic and
continuing with tests of satisfiability modulo a theory, modular
reasoning in combinations of theories (under various conditions
on their shared signatures) and hierarchical reasoning in theory
extensions. We will present the main ideas which appeared in the
literature from a unifying perspective. We will illustrate the
problems and the solutions on examples from mathematics,
verification and knowledge representation.

# Week one 17:00 - 18:30

## Logic and Computation workshop:

Structures and Deduction 2009.

Organizers
- Michel Parigot ()
- Lutz Strassburger ()

Course material: structures_deduction.pdf

Abstract:
The topic of this workshop is the application of algebraic,
geometric, and combinatorial methods in proof theory. In
traditional proof theory, research is focussed on syntax, but in
recent years many researchers have proposed approaches to avoid
"syntactic bureaucracy" in the presentation of proofs. Examples
are proof nets, atomic flows, new deductive systems based on
deep inference, and new algebraic semantics for proofs. These
efforts have also led to new methods of proof normalisation and
new results in proof complexity.

Thus the workshop is relevant to a wide range of people. The
list of topics includes among others: algebraic semantics of
proofs, game semantics, proof nets, deep inference, tableaux
systems, category theory, deduction modulo, cut elimination,
complexity theory, computational interpretation of proofs, etc.

The goal of the workshop is twofold: first, to bring together
researchers from various fields who share the interest in
reducing the dependency of logic from low-level syntax, and
second, to provide an opportunity for PhD students and
researchers to present and discuss their work with colleagues
who work in the broad subject areas that are represented at
ESSLLI.

The workshop is intended to be a sequel of the ICALP-workshop
SD05 in Lisbon 2005 .

## Logic and Computation introductory course:

Games, Action and Social Software.

Teachers
Abstract:
Social software is a term coined by Rohit Parikh for the emerging discipline that investigates the logical, computational and strategic aspects of social mechanisms. The course will give an overview of choice topics in this area, and draw connections with game theory, action logic, epistemic logic, and social choice theory.

Point of departure will be a collection of Discourses on Games, Action and Social Software that is due to appear with Amsterdam University Press, in the Texts in Logic and Games series.

The level of the course will be the level of the discourses in the book, or slightly more advanced.

Each course lecture will be based on one or two of the discourse chapters from the book.

# Week two 9:00 - 10:30

## Logic and Computation advanced course:

Ontologies: Structuring, Modularity, and Heterogeneity.

Teachers
- Stefano Borgo ()
- Oliver Kutz ()

The design of formal ontologies is an interdisciplinary area of
research that draws on logic, philosophy, cognitive science,
linguistics, as well as computer science, with major
applications in the Semantic Web. As the scope and relevance of
ontologies grows, both for supporting Semantic Web applications
and for knowledge-rich processing in general, the issue of
re-using/importing developed ontological components takes on an
ever more critical role. The current solutions being pursued
within OWL-oriented Semantic Web approaches have some severe
limitations in this respect. For the next generation of
ontology-based systems, it will be essential to move beyond
this.

To achieve this, we present major methodologies and techniques
to correctly construct, modify, and relate ontologies -
understood in a broad sense as logical theories formulated in
various formal languages - with an emphasis on heterogeneity,
structuring and modularity, as well as foundations of ontology
design. As illustrative examples, we will discuss prominent
ontologies from the spatial, philosophical and linguistic
domains. These will be analysed and structured using the Common
Algebraic Specification Language (CASL), and shown 'at
work' employing the tool HeTS, offering (heterogeneous)
reasoning support for structured ontologies and providing
powerful new mechanisms for reusing ontological components or
modules. A Live-CD for hands-on experimentation with HeTS will
be distributed to all participants.

## Logic and Computation foundational course:

Logics of Rational Agency.

Teacher
- Eric Pacuit ()

Course material: lori-notes.pdf

Abstract:
Thinking about rational agents interacting over time is at the
center of many research communities represented at ESSLLI. This
course will introduce the main research themes and conceptual
issues surrounding rational agency. The primary objective is to
understand the complex phenomena that arise when rational
agents interact and how to incorporate these phenomena into
formal models. Studying rational agents involves many different
aspects including (but not limited to) action, knowledge,
belief, desires, and revision. This course covers all these
ingredients toward the goal of understanding how these things
work together. Specific topics that will be introduced during
the course include 1. logics of knowledge and belief,
2. information dynamics and belief revision, 3. logics of
preference and preference change, 4. logics of motivational
mental attitudes, and 5. logics of individual and collective
action and 6. group phenomena and issues of social choice. In
fact, not all parts of this story have been developed within
one single discipline. The course will also bring together
several research programs: from philosophy, computer science,
logic, and game theory, and try to see their various
contributions in one coherent manner.

http://ai.stanford.edu/~epacuit/classes/esslli/log-ratagency.html

# Week two 11:00 - 12:30

## Logic and Computation advanced course:

Logics with Counting.

Teacher
Course material: pratt-hartmann.pdf

Abstract:This course presents a survey of decidable fragments of first-order logic with counting quantifiers. Such fragments include: (i) the numerical syllogistic, (ii) the 1-variable fragment with counting, (iii) graded modal logic, (iv) the guarded two-variable fragment with counting and (v) the two-variable fragment with counting. Such logics present special difficulties for the student of computational logic, because their complexity-theoretic analysis often requires specialized techniques. This course will give a comprehensive treatment of these techniques, culminating in a proof that the satisfiability and finite satisfiability problems for the two-variable fragment with counting quantifiers are both NEXPTIME-complete.

## Logic and Computation advanced course:

Reasoning with Probabilities.

Teachers
- Eric Pacuit ()
- Joshua Sack ()

Course material: epprob-outline.pdf

Abstract:
Both logic and probability provide powerful tools for reasoning
about uncertainty in a dynamic environment. Our goal in this
course is to examine logical frameworks that incorporate
probabilistic modeling of multiagent uncertainty. We will then
see how merging these two perspectives on uncertainty can help
clarify various conceptual issues and puzzles (such as the Monty
Hall puzzle or the sleeping beauty problem). The primary
objective is to explore the formal tools used by logicians,
computer scientists, philosophers and game theorists for
modeling uncertainty. We will focus on both the important
conceptual issues (eg., Dutch book arguments, updating with
probability zero events and higher-order probabilities) and the
main technical results (eg., completeness and decidability of
probabilistic modal logics).

Course Outline: The course will cover all of the following
topics:

0. Background in dynamic epistemic logic and probabilistic
models of uncertainty (including issues of measurability and
Dutch book arguments)

1. Various puzzles about probability, beliefs and time
(including the Monty Hall puzzle, the Sleeping Beauty problem
and the Absent-Minded Driver problem)

2. Higher-order probability measures (including a
definition of "common p-belief'' and uses of the concept in game
theory)

3. Modal probabilistic logic (including proofs of completeness,
decidability, and other standard results)

4. Uncertainty in a dynamic environment (including
Bayesian/Jeffrey updates)

5. Updating with probability zero events (including
lexicographic probability distributions, conditional probability
distributions and relations with belief revision models)
6. Dynamic Epistemic Probabilistic Logic (including discussion
of reduction axioms and temporal extensions)

Prerequisites: This is an advanced but self-contained
course. Students will be expected to have had some exposure to
(dynamic) epistemic logic and probabilistic logic. In
particular, it will be assumed that students have already been
introduced to epistemic logic and some of its dynamic extensions
(i.e., public announcement logic); and although we will
introduce many basic concepts of probabilistic theory (e.g.,
measure spaces), it will be expected that students have had
previous exposure to probabilistic models of uncertainty.

http://ai.stanford.edu/~epacuit/classes/esslli/epprob.html

# Week two 14:00 - 15:30

## Logic and Computation advanced course:

Dynamic Logics for Interactive Belief Revision.

Teachers
- Alexandru Baltag ()
- Sonja Smets ()

This course is addressed to students and researchers interested in logics for reasoning about multi-agent belief revision, belief updates and knowledge updates induced by various forms of communication or interaction. It is a foundational course, designed to present to students and researchers from other fields the work done in recent years by a number of researchers on integrating ideas from Belief Revision Theory within the DEL (Dynamic-Epistemic Logic) paradigm. The course is self-contained, not assuming any background knowledge, but presupposing only some general experience or facility with using logical languages, the concepts of syntax and semantics etc. We start by presenting the main notions of "standard DEL", arguing that this logic is appropriate for updating "hard information" (unrevisable knowledge), but that it is inappropriate for "soft information" (possibly false beliefs or defeasible knowledge). We then present "belief-revision models", defining some important epistemic/doxastic notions, considering a number of logical languages for these models, and explaining the relevance of these notions to fundamental issues in contemporary Epistemology, in Computer Science and in the study of language and communication. We present various Belief Update operations and various belief-revision policies proposed by different authors, focusing on one particular proposal (the Action-Priority Update) of great generality and elegance. We present reduction laws (the "dynamic laws of Interactive Belief Revision"), complete axiomatizations, applications to dialogue games and communication strategies, connections with other research areas and open problems.

# Week two 17:00 - 18:30

## Logic and Computation introductory course:

Explanation in Ontology Languages.

Teachers
- Bijan Parsia ()
- Thomas Schneider ()

Course material: explanation.pdf

Abstract:This course will present current research into explanations, which can answer questions such as: "Why do certain entailments follow from my ontology?"; "Why is my ontology inconsistent?"; "Which part of my ontology do I need to modify in order to prevent an undesired entailment?" These questions are of relevance to ontology developers in various domains including bioinformatics, medicine, geography, linguistics. We will focus on proof based explanation techniques and touch on the emerging field of model based explanation.

## Logic and Computation introductory course:

Logics and Agent Programming Languages

Teachers
- Natasha Alechina ()
- Brian Logan ()

Keywords: agent programming languages, logical models of agency, verification

Abstract:
To create a language for programming entities capable of intelligent behaviour (`agents'), researchers and developers must address deep questions such as: what are the basic constituent parts of an intelligent agent; how should the agent `think' (e.g., which deliberation strategy should it employ -- should it plan a precise sequence of actions in advance or should it adopt an abstract plans with gaps `to be filled-in later'); what relationship should there be between the agent's beliefs and its goals, etc. In seeking to address these questions, researchers have drawn heavily on formal models of agents and on agent logics, including epistemic logics, logics of action, dynamic logic, coalition logics etc. For example, the development of agent programming languages such as AgentSpeak were heavily influenced by the BDI (Beliefs, Desires and Intentions) logics developed to understand what an agent's behaviour should be. These interactions have resulted in an extremely fruitful cross fertilisation between work in logic and computation, and the application of logical techniques to address key practical issues such as the verification of agent programs (i.e., will an agent program meet the specification set out by its developers).

This course will address key topics in logics of agent programs including: the Belief Desire Intention model; overview of agent programming languages based on the BDI model; relationship between the operational semantics of BDI-based agent programming languages and logics for reasoning about agents' beliefs and intentions; verification of agent programs using model checking and theorem proving. The course assumes some exposure to modal logic, but no prior knowledge of agent programming languages is required.