Courses' slots:

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.

top

Logic and Computation introductory course:
Non-deterministic Multi-valued Logics.

Teachers
  • Arnon Avron ()
  • Beata Konikowska ()
Abstract:

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.

top

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.

top

Logic and Computation introductory course:
Logics of individual and collective intentionality.

Teachers

External page

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.

top

Week one 14:00 - 15:30

Logic and Computation advanced course:
Game semantics and its applications.

Teacher
  • Andrzej Murawski ()
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.

top

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

External page

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

top

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.

top

Week one 17:00 - 18:30

Logic and Computation workshop:
Structures and Deduction 2009.

Organizers
  • Michel Parigot ()
  • Lutz Strassburger ()

Course material: structures_deduction.pdf

External page

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 .

top

Logic and Computation introductory course:
Games, Action and Social Software.

Teachers

External page

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.

top

Week two 9:00 - 10:30

Logic and Computation advanced course:
Ontologies: Structuring, Modularity, and Heterogeneity.

Teachers
  • Stefano Borgo ()
  • Oliver Kutz ()

External page

Abstract:

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.

top

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

top

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.

top

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

top

Week two 14:00 - 15:30

Logic and Computation advanced course:
Dynamic Logics for Interactive Belief Revision.

Teachers
  • Alexandru Baltag ()
  • Sonja Smets ()
Abstract:

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.

top

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.

top

Logic and Computation introductory course:
Logics and Agent Programming Languages

Teachers
  • Natasha Alechina ()
  • Brian Logan ()

External page

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.

top