Ouro Preto, Minas Gerais, Brazil
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)
Departamento de Matemática,
Universidade Federal de Minas Gerais
(DMAT/UFMG)
Departamento de Computação, Universidade Federal de Ouro Preto
(DECOM/UFOP)
NL-printable sets and Nondeterministic Kolmogorov Complexity
by Eric Allender (Department of Computer Science, Rutgers, the State University of NJ, USA)
P-printable sets were defined by Hartmanis and Yesha and have been investigated by several researchers. The analogous notion of L-printable sets was defined by Fortnow et al; both P-printability and L-printability were shown to be related to notions of resource-bounded Kolmogorov complexity. NL-printability was defined by Jenner and Kirsig, but some basic questions regarding this notion were left open. In this paper we answer a question of Jenner and Kirsig by providing a machine-based characterization of the NL-printable sets. The proof makes use of a simple hashing technique. We apply this same technique to investigate relationships among some resource-bounded notions of Kolmogorov complexity, based on nondeterministic Turing machines.
Quantifying over Quantifiers
by Lauri Hella (Department of Mathematics, Statistics and Philosophy, University of Tampere, Finland)
We study existential and universal quantification over quantifiers, i.e. quantification where the objects quantified over are Lindstrom quantifiers. First we consider the fragment where only existential quantification over quantifiers is allowed, denoted $\Sigma^Q_1$. We show that $\Sigma^Q_1$ includes inflationary fixed-point logic extended with the ability to express that two defined structures are non-isomorphic, and that $\Sigma^Q_1$ is included in existential second-order logic with the same extension.
The logic $\Sigma^Q_n$ is defined as the fragment where we alternate existential and universal quantification for n levels. We show that $\Sigma^Q_{n+1}$ is included in the n-th level of the complexity theoretical exponential hierarchy. We also show that there is a hierarchy on the arity of the quantifier variables, by showing that no fragment of $\Sigma^Q_n$ with restricted arity of the quantifiers can express all $\Sigma^Q_1$ properties.
Calculus of structures and proof-nets
by Jean-Baptiste Joinet (Preuves-Programmes-Systèmes, Université Paris 7, France)
The Calculus of Structures is a new logical formalism developped by A.Gugliemi, L.Strassburger et al. Using the central idea of CS, namely local rewritings of proofs at any depth, but directly in the formalism of Proof-Nets, I will give an alternative characterisation of the Multiplicative fragment of Multiplicative Linear Logic Proof Nets.
Encryption as an abstract data type
by Dale Miller (INRIA/Futurs/Saclay, and Laboratoire d'Informatique, École Polytechnique, France)
At the Dolev-Yao level of abstraction, security protocols can be specified using multisets rewriting. Such rewriting can be modeled naturally using proof search in linear logic. The linear logic setting also provides a simple mechanism for generating nonces and session and encryption keys via eigenvariables. We illustrate several additional aspects of this direct encoding of protocols into logic. In particular, encrypted data can be seen naturally as an abstract data-type. Entailments between security protocols as linear logic theories can be surprisingly strong. We also illustrate how the well-known connection in linear logic between bipolar formulas and general formulas can be used to show that the asynchronous model of communication given by multiset rewriting rules can be understood, more naturally as asynchronous process calculus (also represented directly as linear logic formulas).
Economy and economics in the logic of theory change
by Hans Rott (Institut für Philosophie, Universität Regensburg, Germany)
In this talk, I ask to what extent theory revision may be regarded as a branch of cognitive economics. For a long time, beginning at the latest with the publication of Gärdenfors's Knowledge in Flux in 1988, theory dynamics has been said to be driven primarily by a concern for "informational economy". We take a close look at the role that informational economy has actually played in the development of theories of theory change in the last two decades, and ask whether it should take a (more) important role in their motivation. We discuss the idea of informational economy both with respect to theories and with respect to richer structures representing belief states (identified with theory-revision guiding structures). This view of cognitve economics is contrasted with an alternative view that takes theory change to be a problem of rational choice, or more precisely, of choice based on complete and transitive preferences. It turns out that under this interpretation, theory revision models are indeed amenable to an essentially economic interpretation, but that they inherit the criticism that has been levelled against the classical theory of choice in wider contexts.
Last modified: July 7, 2003, 14:55:33 GMT-0300.
wollic_at_cin.ufpe.br