Swiss Doctoral Program

The first morning of ALCOP 2011 will consist of talks suitable for graduate students in mathematics and computer science, sponsored by the The Swiss Doctoral Program in Mathematics.

Wednesday, 27. April 2011 - University of Bern, B77 (ExWi)


On Proof by Infinite Descent

Alex Simpson, University of Edinburgh

Fermat's method of proof by "infinite descent" is a useful proof technique in number theory. But if a number-theoretic proof is to be formalized in a standard logical theory for arithmetic (such as Peano Arithmetic) then the infinite descent argument has to be recast as a proof by induction. The talk will address the question: are all proofs by infinite descent reducible to proofs by induction?

To turn this into a mathematical question, it is first necessary to formalize the notion of proof by infinite descent. Under a naive formulation, the answer to the question is trivially positive. However, in the talk, I will present an interesting and natural combinatorial notion of proof by infinite descent for which the answer is not trivial.

10.30-11.00 Coffee


A Tutorial on Coalgebra and Coalgebraic Logic

Lutz Schroeder, University of Bremen

Coalgebra has emerged as a unifying framework for generalized relational structures, seen, e.g., as reactive systems, epistemic structures, or collections of individuals. Examples include Kripke frames, Markov chains, concurrent game structures, preference structures, and many others. In this way, coalgebra provides a generic perspective on core notions such as bisimulation, coinduction, and corecursion. Moreover, it supports generic process calculi and generic logics. The latter can in particular take the shape of modal or hybrid logics. While coalgebraic logic in this sense was originally seen as a dedicated specification language for coalgebra, one can reverse this view and regard coalgebra as a generic semantics for a wide variety of modal and hybrid logics found in the literature. There is a well-developed meta-theory of coalgebraic logic that includes not only expressivity results and sound and complete generic axiomatizations, but also generic algorithms and complexity analyses. Computational coalgebraic logic thus serves as the basis for extensions of description logics and temporal logics with expressive means beyond the relational realm. In the present tutorial, we give an introduction to basic concepts of coalgebra and coalgebraic logic, as well as an outlook on current research in coalgebraic description logics.