6th Workshop on Logic, Language, Information and Computation
(WoLLIC'99)

May 25-28, 1999
(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)

Funding 
CAPES, CNPq, Facoltà di Scienze, Univ. di Verona

Organisation
Departamento de Informática, Universidade Federal de Pernambuco (DI-UFPE
Facoltà di Scienze, Università degli Studi di Verona (Sci-Univr
Centro de Lógica, Epistemologia e História da Ciência, Univ. Campinas (CLEHC-UNICAMP)

Title and Abstract of Invited Talks


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 Delta0, 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 A, must, at least in some instances, be rather peculiar.


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