Talks
2008
A small Framework for Proof Checking
We describe a small framework in which first-order theorem provers
can be used for the verification of mathematical theories.
The verification language is designed in such a way that the
use of higher-order constructs is minimized. In this way,
we expect to be able to take advantage of the first order theorem prover
as much as possible.
ps or
pdf .
2007
A study of Landau's Grundlagen der Analysis and AUTOMATH
In his Grundlagen der Analysis, Edmund Landau proves the basic
properties of +.-.*,/ on the natural numbers, rational numbers, the
reals and the complex numbers from the Peano axioms.
In his introduction of addition and multiplication, there is a strange thing:
Both are introdued without reference to the fact that Nat is a free
data type. Especially the introduction of multiplication is a mystery.
In order to check the proofs, we first give a precise description of
Landau's introduction of addition and multiplication. After
this, the proof appears correct to us.
In 1977, the complete Grundlagen have been verified in the Automath system.
So we want to know: What is the mechanism used in Automath for
introducting recursive functions, maybe Van Benthem Jutting used some kind of
additional recursion axiom for introducing addition and multiplication?
We look into the sources of Van Benthem Jutting's translation, and
see that the translation follows Landau's proof very carefully and
that no additional properties were used.
So the question remains: How did Landau/Kalmar manage to get away without
using the fact that natural numbers are freely generated? Are
there more functions definable in that way?
ps or
pdf .
2006
Geometric Resolution: A proof Procedure Based on Finite Model
Search (Talk at Australian National University, November 2006)
The talk is essentially equal to the talk at IJCAR, but it contains
more details.
ps or
pdf .
Geometric Resolution: A Proof Procedure Based on Finite Model
Search (Talk at IJCAR 2006)
In the talk, I present a new calculus for first-order logic with
equality, which is called geometric resolution. The name derives
from the fact that the calculus operates on a normal form which
is remotely related to geometric logic, which was introduced by
Thoralf Skolem.
We show that the calculus is refutationally complete for first-order logic.
A special feature of the calculus is that before proof search,
all function symbols are replaced by relations.
Proof search operates by learning lemmas from failed model construction
attempts.
The calculus is implemented in geo, which got the best newcomer award
at the CASC competition.
ps or
pdf .
Resolution Decision Procedures for Modal Logics
(Habilitationsvortrag, 3 April 2006)
In this talk we introduce the guarded fragment, and
explain how the modal logics K and B can be translated into this
fragment.
We explain why many modal logics cannot be translated into the
guarded fragments.
After that we introduce an improved translation with which most
modal logics can be translated into the guarded fragment.
We characterize the borders of the new translation method.
ps or
pdf .
Verification of a Result Checker for Priority Queues
A priority queue is a container that supports insertion, deletion,
and retrieval of minimal element under a given order.
A result checker (for priority queues) is a datastructure that
stands between the user and the priority queue, and which checks
all interactions between the user and the priority queue.
When the priority queue behaves incorrect, the result checker
will observe this.
We formally verified an ingeneous data structure (developed by
the algorithms and complexity group of our institute),
that performs result checking on priority queues.
The checking datastructure runs in almost linear time, so that
it is guaranteed to run at neglectible cost.
(which is the reason why it has to be so complicated)
Download
ps or
pdf .
2004
Deciding Modal Logics through Relational Translations into GF2
This is an extension of the talk with the same title from 2003.
We present ways of translating modal logics, that appear not to
be in the guarded fragment, into the guarded fragment by optimizing
the relational translation.
The translation works by expressing reachability properties
by regular automata, which can be translated into the guarded fragment.
We attempt to characterize for which modal logics such an
automaton can be constructed.
Download
ps or
pdf .
Translation of Resolution Proofs into Short First-Order Axioms
without Choice Axioms
Talk given in Vienna. This is an improved version of the
talk with the same title below.
ps or
pdf .
2003
Deciding Modal Logics through Relational Translations into GF2
ps or
pdf .
The talk was given at the M4M workshop in Nancy in September 2003.
It talk is based on a joint paper with Stephane Demri.
Translation of Resolution Proofs into Short First-Order Axioms
without Choice Axioms
Talk was given in Dagstuhl, april 2003.
ps or
pdf .
(The slides above, in 2004, are better)
2002
On the generation of Proofs from the Clausal
Normal Form Transformation
The talk was given at CSL 2002 in Edingburgh, Scotland.
ps or
pdf .
2001
Splitting through new Proposition Symbols
The talk was given at LPAR 2001 in Havana.
ps or
pdf .
Translation from S4 into the guarded fragment and the
2-variable fragment
ps or
pdf .
The talk was given in Amsterdam in April 2001.
2000
A resolution based decision procedure for the 2-variable
fragment.
ps or
pdf .
General Lecture on Resolution Based Theorem Proving
ps or
pdf .
1999
Implementation of Resolution
ps or
pdf .
The talk was given in Amsterdam in Mai 1999.