CL Colloquium
Past talks
A machine-checked proof of the enumeration of tame plane graphs
| Speaker: | Tobias Nipkow |
| Homepage: | http://www4.informatik.tu-muenchen.de/~nipkow/ |
| Time and place: | 13-09-2006; 15:00 in HS 10 |
| Description: | Hales' proof of the Kepler conjecture defines a class of tame plane graphs, enumerates that class by computer and checks (again by computer) that none of these graphs constitute a counterexample to the conjecture. This talk reports on the verification of a functional version of Hales' Java program for enumerating tame plane graphs: it is shown that all such graphs are found. This is part of Hales' Flyspeck project to check his whole proof by computer. Throughout the talk we concentrate on the issues that arise when checking mathematical arguments by machine, in particular the challenge of writing programs that are both efficient enough to perform complex searches and enumerations but simple enough that machine-checked correctness proofs become feasible. |
Weighted Automata for Proving Termination of String Rewriting
| Speaker: | Johannes Waldmann |
| Time and place: | 05-09-2006; 10:00 in HS 10 |
| Description: | A weighted finite automaton is obtained from a standard finite automaton by assigning weights from some semi-ring to transitions. By multiplying weights along a path, and adding weights for parallel paths, such an automaton then computes a mapping from words into the weight semi-ring. A standard finite automaton is weighted in the Boolean semi-ring (with two elements). We use weighted finite automata to present a unified treatment of two methods for automatically proving termination of string rewriting: the matrix method and the match bound method. The general scheme is to use a well-founded monotone algebra. The construction is parameterized by the strictness properties of the operations in the weight semi-ring. |
Termination of String Rewriting with Matrix Interpretations
| Speaker: | Dieter Hofbauer |
| Time and place: | 04-09-2006; 10:00 in HS10 |
| Description: | A rewriting system can be shown terminating by an order-preserving mapping into a well-founded domain. We present an instance of this scheme for string rewriting where the domain is a set of square matrices over natural numbers, equipped with a well-founded ordering that is not total. The coefficients of the matrices can be found via a transformation to a boolean satisfiability problem. The matrix method also supports relative termination, thus it fits with the dependency pair method as well. Our implementation is able to automatically solve hard termination problems. |
Nominal Rewriting
| Speaker: | Murdoch James Gabbay |
| Homepage: | http://www.gabbay.org.uk |
| Time and place: | 23-01-2006; 15:15 in 3W04 |
| Description: | Nominal rewriting is a rewriting framework in which object-level alpha equivalence is primitive. This permits a first-order framework (decidability of equality, confluence, critical pair lemma) - which can also express highet-order constructs such as beta-equivalence. For more details kindly see www.gabbay.org.uk |
Proving Combinatorics Theorems in Isabelle/HOL
| Speaker: | Prof. Mizuhito Ogawa |
| Homepage: | http://www.jaist.ac.jp/~mizuhito/ |
| Time and place: | 05-08-2005; 10:00 in 3W04 |
| Description: | In this talk we first present the direction and our experiences in a recent lecture series on theorem provers for graduate students. The latter part of the lecture series focuses on proving several theorems in combinatorics which require the Axiom of Choice (or Zorn's Lemma). We show how they are described in Isabelle/HOL. |