8

**
Brasília,
Brazil**

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

**Organisation**

*Centro de Informática, Universidade Federal de Pernambuco
(CIn-UFPE) *

*Departamento de Matemática, Universidade de Brasília
(MAT-UnB)
*

*Logics of Formal (In)Consistency*

by **Walter Carnielli** (Centro de Lógica, Epistemologia e História da Ciência, Universidade Estadual de Campinas, Brazil)

The logics of formal (in)consistency (**LFI**'s) constitute an
ample class of logics where the concepts of *consistency*
and *inconsistency* appear as new operators $\circ A$ and
$\bullet A$ inside the object language, which permit (given
specific axioms) to logically separate the notions of
*contradictoriness* and of *inconsistency*, and to reason with
such concepts. These logics represent the majority of all
paraconsistent logics existing up to now, if not the most
exceptional ones, and we single out a subclass of them called
**C**-*systems*, as the **LFI**'s that are built over some
given positive basis. This approach clarifies several conceptual
and operational aspects of paraconsistency, helping to understand
that the gist of paraconsistent logic lies on the Principle of
Explosion, rather than on the Principle of Non-Contradiction (to
be also distinguished from the Principle of Non-Triviality).

Syntactical formulations of the main **C**-systems based on classical
logic are presented, showing how several well-known logics in the
literature can be recast as such **C**-systems, and how they
can be used to faithfully reproduce all classical inferences,
despite being themselves only fragments of classical logic. We
also discuss some semantical aspects, sketch the completeness with
respect to valuation semantics and with respect to the new
*possible-translations semantics*, and show the usefulness of
**LFI**'s in applications to databases, knowledge representation and
belief change.

*Graphs Trees and Monadic Second Order Logic:
Recent results and open problems*

by **Bruno Courcelle** (Université Bordeaux-1, LaBRI, France)

By considering a graph as a relational structure consisting
of the set of vertices as domain and of a binary relation
representing the edges, one can express graph properties in logical languages like First-Order Logic or Second-Order Logic. The purpose of *Descriptive Complexity*
is to relate the complexity of graph
properties (or more generally of properties of finite relational structures)
with the syntax of their logical expressions, and to characterize complexity
classes in logical terms, independently of computation models
like Turing machines.

As main logical language, we will consider *Monadic Second-Order Logic*, i.e., the extension of First-Order Logic with variables
denoting sets of elements of the considered structures. Despite the fact that it does not correspond exactly to any complexity class, this language enjoys a number of interesting
properties.

First, it is rich enough to express nontrivial graph properties like planarity, vertex $k$-colorability (for fixed $k$), connectivity, and many others (that are not expressible in First-Order Logic).

Second, because the verification of a property
expressed in Monadic Second-Order Logic
can be done in linear time on certain graphs constructed
in an appropriate hierarchical way (for an example, the graphs
of tree-width at most $k$). This linearity result extends to
*optimization problems* consisting in
computing for a given graph, the minimum (or maximum) cardinality of a set of vertices satisfying a fixed monadic second-order formula with one free set variable.

*Counting problems*
consisting in counting the number of sets satisfying a given formula
can also be handled efficiently. This applies to NP-complete problems like
Hamiltonicity or to the Traveling Salesman Problem; to take another example,
structured ("goto"-less) programs can be represented by graphs of tree-width
at most 6, and register allocation can be done efficiently for them (M. Thorup). However, although
the algorithms are linear for fixed tree-width, the constant factors depend
exponentially or more upon the
tree-width and the sizes of the formulas.

Finally, Monadic Second-Order Logic is an essential tool for studying context-free graph grammars.

These interesting algorithmic and grammatical properties are based
on the equivalence between monadic second-order logic and
finite automata on finite trees (i.e., trees that represent
finite well-formed terms written over a finite set of operation symbols).
A graph constructed from "small" basic graphs by means of graph
operations (generalizing the concatenation of words) can be considered
as the value of a finite term.
We are interested by graph operations such that the corresponding mapping
from trees (representing terms) to graphs is *MS-compatible*, which means that for every monadic second-order formula $P$ expressing a graph property, one can construct an "equivalent" monadic second-order
formula over trees
expressing that the graph that is the value of the considered tree satisfies $P$.

In many cases we have a stronger property than MS-compatibility:
the graph can be defined "in the tree" by monadic second-order formulas.
We say that the graph is obtained from the tree by
a *Monadic Second-Order definable transduction*, an *MS-transduction* in short.

We will review the various operations on graphs for which the evaluation mapping is an MS-transduction. They are the binary operation of union of two disjoint graphs, a unary operation that fuses all vertices of a graph satisfying some predicate $p$, unary operations like the edge-complement that redefine the edge relation by quantifier-free formulas.

The two main classes of context-free graph grammars, the *HR Grammars*
(HR stands for *hyperedge replacement*) and the *VR Grammars*
(VR stands for *vertex replacement*) can be defined by systems of recursive
set equations over these operations.
The corresponding classes of sets of graphs are closed under
MS-transductions, and are generated from the set of binary trees
by such transductions. Hence, the classes HR and VR are robust and have
characterizations independent of the graph
operations used to build the corresponding systems
of equations. This establishes a strong connection between
context-free graph grammars and monadic second-order logic.
Certain "classical" families of graphs can be described by context-free
grammars. However, many interesting families like that of all finite
planar graphs cannot be represented by a single context-free grammar.
This is unavoidable unless P = NP.

The graph operations on which VR-grammars are based yield the notion
of *clique-width* of a graph. This is a complexity measure comparable to tree-width, but stronger in the sense that, for a set of finite graphs, bounded tree-width implies bounded clique-width, but not vice versa. It serves as a parameter in the sense
of *Parametrized Complexity*, defined by Downey and Fellows. Problems
expressible in monadic second-order logic are thus parametrically tractable.

We will discuss a still open conjecture by D. Seese saying that if a set of finite or countable graphs has a decidable satisfiability problem for monadic second-order formulas, then it is obtained from a set of trees by an MS-transduction. We will present the main special cases (that of planar graphs for instance) for which this conjecture is known to hold. This will be the occasion to review some applications to this field of the deep results of Robertson and Seymour on graph minors.

After having presented these situations where graphs are defined
from trees by MS-compatible
mappings, we will then consider cases where
a tree is defined from a finite or countably infinite directed graph,
by means of an MS-compatible
mapping, namely the *Unfolding*. Intuitively, the graph represents a process and the unfolded tree, formally defined as the (usually infinite) tree of
finite paths originating at a specified initial vertex, represents its behaviour.
We will present methods for defining new MS-compatible mappings on graphs
motivated by formalization of semantics and program verification.

We will conclude with the presentation of some open problems related to this topic.

**Note**: Most of these results, stated here for "graphs" for simplicity, actually hold for relational structures.

**Main References**

**B. Courcelle**: The expression of graph properties and graph transformations
in monadic second-order logic, Chapter 5 of the *Handbook of graph grammars
and computing by graph transformations, Vol. 1 : Foundations*, G. Rozenberg ed.,
World Scientific (New-Jersey, London), 1997, pp. 313-400.

**B. Courcelle, J. Makowsky**: Operations on relational structures and their compatibility
with monadic second-order logic, 2000, submitted.

**B. Courcelle, J. Makowsky, U. Rotics**: Linear time solvable optimization problems
on certain structured graph families,
*Theory of Computer Science* (formerly *Mathematical Systems Theory*) **33** (2000) 125-150.

**B. Courcelle, S. Olariu**: Upper bounds to the clique-width of graphs, *Discrete Applied Mathematics* **101** (2000) 77-114.

**B. Courcelle, I. Walukiewicz**: Monadic Second-Order Logic, graph coverings and unfoldings of transition systems, *Annals of Pure and Applied Logic* **92** (1998) 35-62.

**R. Downey, M. Fellows**: *Parametrized complexity*, Springer-Verlag, 1997.

**D. Seese**: The structure of the models of decidable monadic theories of graphs, *Annals of Pure and Applied Logic* **53** (1991) 169-195.

Full texts of submitted or unpublished papers and other references can be found from:

http://dept-info.labri.u-bordeaux.fr/~courcell/ActSci.html.

A list of results on clique-width is maintained on the page: http://www.laria.u-picardie.fr/~vanherpe/cwd/cwd.html

*Confluence as a cut elimination property*

by **Gilles Dowek** (INRIA, France)

Confluence and cut elimination both express that provable propositions have analytic proofs, i.e. proofs using no external arguments. In particular both properties can be used to prove that some theories are consistent. We show in this talk that the confluence of a rewrite system can indeed be defined as a cut elimination property for a simple logical formalism associated to this rewrite system.

*Braided linear logic*

by **Arnaud Fleury** (Facoltà di Scienze, Università degli Studi di Verona, Italy)

This work formalizes the exchange rule over a non commutative calculus (that is to say without exchange) in such a way that the application of a permutation will not be forgotten when considering the final proof from a global perspective. This leads to a consideration of proof graphs as embedded in the three dimensional space.

*
Some new trends in mathematical fuzzy logic
*

by **Petr Hájek** (Institute of Computer Science, Academy of Sciences, Czech Republic)

Whereas the "basic fuzzy logic" BL is a well-developed logic of continuous t-norms (as truth-functions of cojunction), recently investigation of logics based on left-continuous t-norms has been started by Esteva and Godo, with further contributions by Gottwald, Jenei, Montagna and others. Left continuity is a necessary and sufficient condition for the existence of the residuum of the t-norm as the coresponding truth-function of implication. The most prominent left-contiuous non-continuous t-norm was discovered by Fodor in mid-ninetees. Existing results will be surveyed; left-continuous generalizations of the three famous logics (Lukasiewicz, Gódel, product logic) will be investgated. Particularly, the "generalized product logic" will be considered.

*Automata on Guarded Strings*

by **Dexter Kozen** (Department of Computer Science, Cornell University, USA)

Regular sets of guarded strings were introduced by Kozen and Smith in 1996 as a model for Kleene algebra with tests (KAT). Guarded strings are like ordinary strings, except that between each letter there is an atom of a free Boolean algebra. The regular sets of guarded strings play the same role in KAT as the regular sets of ordinary strings do in Kleene algebra.

In this talk I will introduce finite-state automata on guarded strings and give several basic constructions, including determinization, state minimization, and an analog of Kleene's theorem. These results are generalizations of the analogous results in classical automata theory. I will then show how automata on guarded strings can be used to prove PSPACE-completeness of a Linear Logic for partial correctness. I will also show that a central result of the theory of BDDs (Boolean decision diagrams), namely that reduced ordered BDDs are unique, is a special case of the Myhill-Nerode theorem for a class of automata on guarded strings.

*Pseudo-finite model theory*

by **Jouko Väänänen** (Department of Mathematics, Helsinki University, Finland)

We consider the restriction of first-order logic to models, called pseudo-finite, with the property that every first-order sentence true in the model is true in a finite model. We argue that this is a good framework for studying first-order logic on finite structures. We prove a Lindström Theorem for extensions of first order logic on pseudo-finite structures and discuss the prospects of abstract pseudo-finite model theory.

*Last modified: July 11, 2002, 09:30:33 GMT-0300.*