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

• Andrzej Murawski ()

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 advanced course:
Reasoning in complex theories and applications.

• Viorica Sofronie-Stokkermans ()

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

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.

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

• Stefano Borgo ()
• Oliver Kutz ()

External page

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 advanced course:
Logics with Counting.

• Ian Pratt-Hartmann ()

Course material: pratt-hartmann.pdf

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.

• Eric Pacuit ()
• Joshua Sack ()

Course material: epprob-outline.pdf

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

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

• 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.