(WoLLIC'99)

(Tutorial Day: May 25th)

**
Hotel Simon, Itatiaia National Park, Rio de Janeiro, Brazil**

**(In conjunction with XII Encontro Brasileiro de Lógica - EBL'99)**

**Scientific Sponsorship**
*Interest Group in Pure and Applied Logics (IGPL)**European Association for Logic, Language and Information (FoLLI)**Association for Symbolic Logic (ASL)**Sociedade Brasileira de Computação (SBC)**Sociedade Brasileira de Lógica (SBL)*

*Introduction to Game Semantics*

by **Samson Abramsky** (Laboratory for Foundations of Computer Science, Division of Informatics, Edinburgh University, Scotland)

Game semantics has emerged as a powerful paradigm for giving semantics to a variety of logical systems and programming languages. It has been used to prove full completeness results - completeness at the level of proofs, not moerely provability - and to give the first syntax-independent constructions of fully abstract models for a spectrum of programming languages ranging from purely functional languages to languages with non-functional features such as control operators and references. There are also applications to the semantics of branching quantifiers and ``independence-friendly'' logics, which have connections to the semantics of natural language.

In this tutorial, some basic concepts of game semantics will be introduced, and a survey of some of the applications will be given.

*Stability and Finite Model Theory*

by **John Baldwin** (Department of Mathematics, Statistics and Computer Science, University of Illinois at Chicago, USA)

We will describe some of the concepts of stability theory which are
particularly relevant to applications in finite model theory. The
fundamental step is to switch the focus from logics (discussion of
all valid sentences and all finite models) to the classification of
theories (restrictions to certain (logically definable) subclasses of
models). Some of the key techniques which have been developed in infinite
stability theory include:
the stability hierarchy, definability of types, Morley sequences and
indiscernibles. One particular notion which seems appropriate for
the finite context are the classification of formulas by certain
combinatorial
properties: the order property, the independence property, the finite
cover property.
We will consider the work of Baldwin and Benedikt on `embedded finite
model theory'. Bounds on the expressive power of first-order logic over
finite structures and over ordered finite structures were extended,
by generalizing to the situation where the finite structures are embedded
in an infinite structure *M*, where *M* satisfies some simple
combinatorial properties studied in model-theoretic stability theory.
They showed first-order logic over finite structures embedded in a
*stable* structure has the same generic expressive power as
first-order logic on unordered finite structures.
It follows from this that having the additional structure
of, for example, an abelian group or an equivalence relation,
does not allow one to define any new generic queries.
They also showed first-order logic over finite structures embedded in
any model *M* that *lacks the independence property* has
its expressive power bounded by first-order
logic over finite ordered structures.
In particular, this implies that common queries such as parity
and connectivity cannot
be defined for finite structures embedded in a model without the
independence property. The tutorial will aim to expound the kinds of
questions concerning embedded finite models that are accessible to the
techniques of stability theory.

(For the slides, click here)

*Markov Decision Processes and Bayesian Networks*

by **Craig Boutilier** (Department of Computer Science, University of British Columbia, Canada)

Markov decision processes provide a conceptually elegant way of modeling stochastic sequential decision problems. In this tutorial, I describe the basic model and some of the dynamic programming algorithms that have been developed to construct optimal policies. Unfortunately, because MDPs and their solution algorithms require explicit state space enumeration, they do not scale well when the state of the system to be controlled in described in terms of a set of random variables (Bellman's "curse of dimensionality"). We describe Bayesian networks as a way of compactly representing joint distributions and how they can be used to represent the dynamics of a stochastic transition system in much they same way that STRIPS or the situation calculus are used to describe deterministic transition systems.

*A Crash Course in Distributive Lattices *

by **Francisco Miraglia** (Instituto de Matemática e Estatística, Universidade de São Paulo, Brazil)

*Program*: Lattices and Distributive Lattices. Heyting and Boolean
algebras. Complete Heyting Algebras (cHa; also called frames or locales).
If possible, we shall present the concept of presheaf of sets over a cHa.

In the advanced talk I shall present joint work with Xavier Caicedo, a description of which appears in the abstracts page.

*Bounded Arithmetic, Nonstandard Models *

by **Alan Woods** (Department of Mathematics, University of Western Australia, Australia)

Bounded Arithmetic refers to the fragment of Peano Arithmetic obtained
by restricting the induction schema to bounded quantifier formulas.
Studying this axiom system and its extensions appears to offer real
hope of eventually being able to analyse the principles required in
proofs of number theoretic sentences.

These tutorial lectures will survey what is known about Bounded Arithmetic,
and what we might hope to know. (There are many open problems.) The
emphasis
will be the number theoretic aspects, trying to give a feel for what is
"routine" to prove, and what is not, while also touching on some of the
basic properties of its nonstandard models, i.e., models other than the
standard natural numbers.

*Last modified: March 15, 2002, 09:57:50 GMT-0300.*