(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)*

*Concurrent games and Full Completeness*

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

A concurrent games model of Linear Logic will be presented, and a full completeness result will be described.

*Finite and Infinite Model Theory*

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

We will discuss recent work relating stability theory and finite model theory. This includes work by Hytinnen, Djordevich, Ziegler, Casanovas, Hedman, Benedikt, Shelah and the author. The applications in finite model theory fall into three categories: i) embedded finite model theory, ii) stability theory for complete theories in finite variable logic (with finite models) and iii) relations between stability theory and 0-1 laws.

(For the slides, click here)

*Abstraction and Decomposition Techniques for Markov Decision Processes*

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

Recent interest in decision theoretic planning has focused on developing planning models in which uncertainty, competing objectives and process-oriented planning problems can be adequately represented and solved. Markov decision processes (MDPs) have provided effective conceptual and computational underpinnings for much of this work, but the combinatorial nature of state spaces often makes their direct use infeasible. In this talk, I summarize recent developments in which AI representations---for instance, Bayesian networks and decision trees---are exploited in standard dynamic programming techniques for MDPs, allowing the natural formulation and solution of feature-based decision problems. I will focus, in particular, on several methods of exact and approximate abstraction, in which relevant distinctions in feature space are detected automatically. These techniques allow rather fine-grained control of the trade-off between solution quality and computation time in decision theoretic planning. I will also briefly desccribe some related ideas that have the potential to make the solution of MDPs more feasible, including decomposition and reachability analysis.

*Intrinsic theories: a methodology for reasoning about functional programs and their computational complexity*

by **Daniel Leivant** (Department of Computer Science, Indiana University, USA)

We present a general methodology for reasoning about functional programs, which uses as axioms only the properties most intrinsic to the data type in hand, and treats programs as auxiliary axioms. Its advantages include expressive flexibility, minimal axiomatics, dispensing with coding for reasoning about partial functions, data genericity, and a clear conceptual framework for machine-independent characterizations of a wide spectrum of computational complexity classes.

*A Lattice-Theoretic Concept of Logical Connective*

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

Our purpose here is to point the way to an algebraic theory of logical
connectives. The guiding idea is that a **logical** connective should be
*homogeneous and local*, that is, it should behave similarly on
similar structures and its global behavior should be locally determined.
Consider, for example, a complete Heyting algebra (cHa) $\Omega$ and let
$Sh(\Omega)$ be the topos of sheaves over $\Omega$. It is well known ([FS])
that intuitionistic, even higher order, logic has a semantic interpretation
in $Sh(\Omega)$. Moreover, the subobject classifier in $Sh(\Omega)$ is the
object \mbox{\boldmath $\Omega$}, called by Fourman and Scott the sheaf of
propositions and consisting of all restriction maps determined by the
meet operation of $\Omega$. A **logical connective** should operate on
truth values, that is, sections of \mbox{\boldmath $\Omega$}, in such a way
that it is uniformly defined on the set of sections (homogeneous) and
respects restriction in this sheaf (local). Thus, we are led to define a
*n*-ary connective in $Sh(\Omega)$ as a **sheaf morphism**

\mbox{\boldmath $\Omega$}^{n} => \mbox{\boldmath $\Omega$}.

It turns out that this definition is equivalent to a nice functional
equation on the cHa $\Omega$, which can be written using only the
meet operation. Hence, it makes sense in a much wider class of lattices.
We can, therefore, study this notion of connective in any class of lattices,
although we shall concentrate here on distributive ones.

Note that an **intuitionistic connective** should be one that lives in
$Sh(\Omega)$, for **all** $\Omega$. Via the functional equation mentioned
above, we define the concept of **connective with respect to a category**,
together with relative versions of these ideas.

A brief summary of the paper is as follows. In section 1 we define connectives
in the topos of sheaves over a cHa and prove the equivalence of this notion
with the solution of a certain functional equation over the cHa \om.
This in turn yields the notion of \y n-ary connective
in a rather general context, although we shall here
concentrate in developing the properties of connectives in distributive
lattices. In section 2 we discuss the concept of
connective relative to *acceptable* categories -- certain
categories of distributive lattices --, encoding the notion of
connective that is meaningful in a category of "truth values".
In section 3 we describe the connectives in acceptable categories with free
objects generated by finite sets.
As a consequence, connectives of any arity in distributive lattices,
Boolean algebras and Heyting algebras are completely described.
Section 4 is devoted to the classification of connectives in the categories of
cHa's, complete Boolean algebras, sober topological spaces and topological
spaces in general. Section 5 studies connectives in the
category of linear orders, applying our results to classify
*n*-ary connectives in Post algebras of (fixed) finite order.

**References**

[FS] M. Fourman, D.Scott, *Sheaves and Logic*, Springer
Lecture Notes in Mathematics 753, 303-401, 1979.

*Bounded Arithmetic from a Rational Perspective*

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

There are many properties of the nonnegative integers which are not
known to be theorems, or non-theorems, of natural weak systems of
arithmetic, such as the axiom system I Delta_{0}, whose main axiom is
the schema of induction restricted to bounded quantifier formulas.
Any nonstandard model *M* of such axioms, has a corresponding field *F*
of fractions, playing the role of "rational numbers". An interesting
question is the extent to which these axioms of bounded arithmetic must
be augmented in order that various properties of the standard
rationals must also be true of *F*.

An example is the local-global principle (also known as the
Hasse-Minkowski principle) which gives a necessary and sufficient
condition for the existence of a nontrivial solution in rational
numbers to quadratic form equations. This principle is of particular
significance, firstly because it generalizes questions considered by
other researchers, and secondly because having "enough" of the
local-global principle available seems to be the main extra ingredient
required to make Julia Robinson's first order definition of the natural
numbers within the rational field work. The presence of such a
definition allows a change of perspective, in which the field *F* (which
necessarily will satisfy certain axioms *A* in the language of fields)
is regarded as fundamental, and the underlying model *M* is recovered
as the elements satisfying the definition.

If the axioms *A* have the property that there is such a definition,
but not by means of any universal formula, then the behaviour of the
corresponding rings of integers, when a field *F* satisfying *A* is extended
to another model *F ^{'}* of

*Last modified: March 15, 2002, 09:56:22 GMT-0300.*