Abstract of Invited Talks

Alex 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