Hotel Simon, Itatiaia National Park, Rio de Janeiro, Brazil
(In conjunction with XII Encontro Brasileiro de Lógica - EBL'99)
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.