Fontainebleau Campus of Université Paris 12, France
Scientific Sponsorship
Interest Group in Pure and Applied Logics (IGPL)
European Association for Logic, Language and Information (FoLLI)
Association for Symbolic Logic (ASL)
European Association for Theoretical Computer Science (EATCS)
Sociedade Brasileira de Computação (SBC)
Sociedade Brasileira de Lógica (SBL)
Funding (expected)
??
Organisation
Centro de Informática, Universidade Federal de Pernambuco
(CIn-UFPE)
Laboratoire d'Algorithmique, Complexité et Logique, Université Paris XII
(LACL-Paris12)
Differential lambda-calculi and interaction nets
by
Thomas Ehrhard (Institut de Mathématiques de Luminy, Université de la Mediterranée Aix-Marseille II, France)
Vector space web-based models of linear logic strongly suggest to consider extensions of linear logic and lambda-calculus where proofs (programs) can be differentiated. We shall present such a formalism and show how differentiation in the lambda-calculus is related to linear substitution and linear head-reduction (a notion of reduction implemented in particular by Krivine abstract machine).
Using Lafont's interaction nets, we shall also give a "graphical" version of such a differential formalism, where differential constructs appear as exact duals of the standard linear logic exponential operations of dereliction, weakening and contraction. This syntactic symmetry is preserved by reduction rules (cut-elimination) as well.
Living with Paradoxes
by
Manfred Kerber (School of Computer Science, The University of Birmingham, UK)
A good knowledge representation system has to find a balance between expressive power on the one hand and efficient reasoning on the other. Furthermore it is necessary to understand its limitations and problems. A logic which contains strings is very expressive and allows for very natural representations, which in turn allow for appropriate reasoning patterns. However, such a system has the feature that it is possible to formulate self-referential paradoxes in it. This can be considered as a strength and as a weakness at the same time. On the one hand it is a positive aspect that it is possible to represent paradoxes, which can be formulated in natural language. On the other hand it is necessary to be careful and not to trivialize the logical system. In the talk different aspects of knowledge representation which allows self-referentiality will be discussed. A system will be presented which is a pragmatic compromise between expressive power on the one hand and simplicity and efficiency of the reasoning process on the other hand. It is built on a three-valued system that makes it possible to use reasoning techniques from classical first-order logic.
Probabilistically checkable proofs over the reals
by
Klaus Meer (University of Southern Denmark, Odense, Denmark)
Probabilistically checkable proofs (PCPs) have turned out to be of great importance in complexity theory. On the one hand side they provide a new characterization of the complexity class NP, on the other hand they show a deep connection to approximation results for combinatorial optimization problems. In this talk we study the notion of PCPs in the real number model of Blum, Shub, and Smale. The existence of transparent long proofs for the real number analogue NP$_{\mathbb R}$ of NP is discussed.
Deciding nondeterministic hierarchy of deterministic tree automata
by
Damian Niwinski (Department of Mathematics, Informatics and Mechanics, Warsaw University, Poland)
While most of decision questions about finite automata running on words (finite or infinite) is known to be decidable, we know much less about finite automata on trees. For instance, simplification of a Rabin automaton to a Buchi one is sometimes possible (over infinite trees), but no effective procedure for this task is known.
The problem appears to be easier if the input automaton is deterministic: for that case T.Urbanski gave an algorithm which transforms a given Rabin automaton to an equivalent (nondeterministic) Buchi automaton, or says that it is impossible. In the present paper we extend this result to the whole hierarchy of Rabin's indices (or, equivalently, Mostowski's indices of parity automata). That is, we show that, given a deterministic parity automaton, one can compute the minimal index of an equivalent nondeterministic parity automaton.
(Joint work with Igor Walukiewicz)
Membrane Computing. Power and Efficiency
by
Gheorghe Paun (University of Sevilla, Spain, and Institute of Mathematics of the Romanian Academy, Romania)
A powerful trend in informatics is to search new computing ideas, models, paradigms in biology, and this area is curently known under name of Natural Computing. Membrane Computing (MC) is part of this enterprise. Its goal is to abstract computing models from the structure and the functioning of the living cell.
The present paper is an informal introduction to MC, presenting the basic ideas, the central (mathematical) results, and the main directions of research. A case study is presented in the appendix: the way {\tt SAT} problem can be solved in linear time by a specific type of MC systems.
Compositional Methods (slides)
by
Alexander Rabinovich (School of Computer Science, Tel Aviv University, Israel)
Composition Theorems are tools which reduce sentences about some compound structure to sentences about its parts. A seminal example of such a result is the Feferman-Vaught Theorem which reduces the first-order theory of generalized products to the first order theory of its factors and the monadic second-order theory of index structure. Another prominent example is the Shelah Theorem which reduces the monadic second-order theory of the generalized sum to the monadic second-order theories of the summands and of the index structures.
Last modified: July 30, 2004, 10:10:20 GMT-0300.