Abstract of Invited TalksAlex Borgida,
Dept. of Computer Science, Rutgers University
Description Logics: formal foundations and applications
Abstract: Description logics (DLs) are a family of knowledge representation
formalisms that focus on representing individuals, related by (binary)
relationships, and grouped into concepts. Some distinguishing feature of DLs
are that (i) complex concepts (and relationships) are built as variable-free
terms using concept constructors (resembling the way types are built with
type constructors), and (ii) research has uncovered numerous sets of
constructors which allow interesting conceptual models to be built, yet for
which reasoning is decidable.
After briefly reviewing the motivation for DLs, and some of the bewildering
variety of surface syntaxes, we consider their logical aspects:
denotational semantics, relevant deduction problems, and different kinds of
inference procedures, including one based on tableaux. We also relate
various DLs to propositional dynamic logics, and FOL with counting
quantifiers but only 3 variable symbols.
Finally, we review some of the applications where DLs have been found to be
useful (configuration, database schema design, medical terminologies) and
tomorrow's promise (or is it hype?): as the technology supporting the vision
of the Semantic Web.
Alessandra Carbone,
Department of Computer Science, Universite Pierre et Marie Curie
Group Theory and Classical Proofs
Group theory suggests some explanation of the complexity of
classical proofs both for the propositional and the predicate case.
we shall state the problem and establish the connection between the
geometric methods developed in the combinatorial theory of small
cancellation and the propositional resolution calculus
and, the theory of finitely presented groups and the predicate calculus.
These results should be considered as a first step towards a
definition of formal proofs as high dimensional complexes.
Alessandra Carbone,
Department of Computer Science, Universite Pierre et Marie Curie
Genome synthesis and genomic functional cores
Abstract: The project of synthesizing a bacterial genome which
can survive in the laboratory and can realize desired metabolic
cycles, has been announced three years ago by Venter, Smith and
Hutchison. It asks for clearing out certain basic biological mechanisms
of living cells. The problem demands to search for the minimal set
of genes that are essential to the life of a microbial organism.
Laboratory experiments realized on specific bacteria allowed to propose
some minimal gene set. Independently, comparative genomics also proposed
some minimal set of genes. But both these "solutions" present
some intrinsic problem.
We shall present some simple mathematical ideas based on Gibbs sampling,
that allow to detect genomic signatures for sets of genes and sets of
organisms, and to predict genomic functional cores which are specific to
different microbes. Within these sets, one finds many of the genes
characterized with experiments and genome comparison, but also
genes which might be non-orthologous or whose function might not
be characterized yet. More generally, our computational approach
leads to characterize essential metabolic pathways through a purely
statistical analysis of complete genomes which is independent from
biological assumptions.
Martín Escardó,
School of Computer Science, University of Birmingham
Algorithmic topology of program types
Abstract: Topological ideas pervade computation with infinite data,
for example higher-type computation or real-number computation. We
develop these topological ideas from an algorithmic point of view. We
show that not only notions but also theorems in topology have
algorithmic readings. This leads to surpring, and perhaps
counter-intuitive, computational conclusions. For instance, it turns
out that the higher type ((Integer -> Bool) -> Integer) has decidable
equality (and there are computer programs in e.g. ML, Haskell and
ocaml that solve this decision problem). This has to do with the fact
that the topology of the type (Integer -> Bool), namely the Cantor
topology, is compact. Of course, the type (Integer -> Bool) doesn't
have decidable equality (which has to do with the fact that the
topology of the type Integer is not compact). In addition to
developing particular examples such as these, in the talk we will
sketch a general theory of algorithmic topology, briefly hinting
relationships with various fields in the theory of computation,
including Kleene-Kreisel functionals, domain-theoretic denotational
semantics, and operational semantics. We don't presuppose background
on topology for this talk.
Philippa Gardner
Context logic and tree update
Abstract: TBA
Achim Jung
On the interplay of logic and information: a topological analysis
Abstract: TBA
Louis Kaufmann
Spin networks in quantum computation
Abstract: TBA
Louis Kauffman
Biologic
Abstract: TBA
Michael Moortgat
Symmetries in natural language syntax and semantics:
the Lambek-Grishin calculus
Abstract: TBA
Paulo Oliva
Computational interpretations of classical linear logic
Abstract: TBA
John Reif,
Department of Computer Science, Duke University
Autonomous programmable biomolecular devices using self-assembled
DNA nanostructures Specifying properties of data
Abstract: This talk overviews the past and current state of a selected
part of the emerging research area of the field of biomolecular
devices. We particularly emphasize molecular devices that are:
• Autonomous: executing steps with no exterior mediation after starting, and
• Programmable: the tasks executed can be modified without entirely
redesigning the nanostructure.
We discuss work in this area that makes use of synthetic DNA to self-assemble
into DNA nanostructure devices. Recently, there have been a series of quite
astonishing experimental results - which have taken the technology from a state
of intriguing possibilities into demonstrated capabilities of quickly increasing
scale. We discuss various such programmable molecular-scale devices that achieve:
• computation,
• 2D patterning, and
• transport.
This talk will presented for a computer science audience, and particularly emphasizes
the unique impact of computer science to this quickly evolving and interdisciplinary
field.
Papers (see survey papers 44 & 45) discussed can be downloaded from URL:
http://www.cs.duke.edu/~reif/vita/topics/biomolecular.html
Yde Venema
A modal distributive law
Abstract: TBA
