A coinductive approach to exact real number computation

A coinductive approach to exact real number computation

Abstract

Coinduction is a concept of increasing importance in mathematics and computer science, in particular in non-wellfounded set theory, process algebra and database theory. Probably the best-known example of a coinductive relation is bisimilarity of processes. In this talk I present an application of coinduction to exact real number computation. Intuitively, coinduction is about deconstructing, or observing data, or describing how a process evolves. This is in contrast to induction, which is about constructing data. A real number, say pi, is a typical candidate for coinduction. We cannot construct pi (exactly), but we can make observations about it, by, for example, successively computing digits of pi. Similarly, a computable continuous functions on the real numbers can be viewed as a coinductive process: we successively compute digits of the output while reading digits of the input. In fact, it turns out that the computation of a single correct output digit is an inductive process. Therefore, continuous real functions are described by a combination of induction and coinduction.

Algorithmic Approaches for Protein Structure Analysis and Design

Algorithmic Approaches for Protein Structure Analysis and Design

Abstract

A general introduction will be given about some basic principles of molecular biology such as DNA/RNA, genes and proteins. Examples will be presented to illustrate how the molecular machinery is related to cellular function and how its misfunction is connected to disease. This connection illustrates the importance to understand in depth molecular structure and function. The second part will be dedicated to our computational approaches to understand the molecular design of proteins, comprising, among others, string representations, clustering and Monte Carlo techniques.

Deductive Temporal Reasoning with Constraints

Abstract

Often when modelling systems, physical constraints on the resources available are needed. For example, we might say that at most 'n' processes can access a particular resource at any moment or exactly 'm' participants are needed for an agreement. Such situations are concisely modelled where propositions are constrained such that at most 'n', or exactly 'm', can hold at any moment in time. This talk describes both the logical basis and a verification method for propositional linear time temporal logics which allow such constraints as input. The complexity of this procedure is discussed and case studies are examined. The logic itself represents a combination of standard temporal logic with classical constraints restricting the numbers of propositions that can be satisfied at any moment in time. We discuss restrictions to the general case where only 'exactly one' type constraints are allowed and extensions to first-order temporal logic.