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)

Funding
,

Organisation
Centro de Informática, Universidade Federal de Pernambuco (CIn-UFPE) 
Departamento de Matemática, Universidade de Brasília (MAT-UnB)

Title and Abstract of Invited Talks

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.