Presentations
2022
Generating Tokenizers with Flat Automata
We introduce flat automata for automatic generation of tokenizers.
Flat automata are a simple representation of standard finite automata.
Using the flat representation, automata can be easily constructed,
combined and printed.
Due to the use of border functions,
flat automata are more compact than standard automata in the case where
intervals of characters are attached to transitions, and
the standard algorithms on automata are simpler.
We give the standard algorithms for tokenizer construction with automata,
namely construction using regular operations, determinization, and
minimization, and prove their correctness.
The algorithms work with intervals of characters,
but are not more complicated than their counterparts on single characters.
It is easy to generate C++ code from the final deterministic automaton.
All procedures have been implemented in C++ and are publicly available.
The implementation has been used in applications and in teaching.
This presentation was given at
GandALF 2022 .
These are the slides.
Maphoon: A C++ based Parser Generator
I describe a toolset for the implementation of parsers,
called Maphoon.
In computer science, nearly everything is a tree.
Unfortunately, we often have to represent these trees as text.
Extracting the tree structure from a text is called parsing.
Maphoon is a toolbox that consists of two parts: The first
part is a library that contains an automaton-based implementation
of classifiers. A classifier cuts the input
into pieces, and classifies the pieces.
The classifier does not create a complete tokenizer, because that would
result in a lack of flexibility, that would make the resulting
tokenizers unusable in practice.
Classifiers are easy to use, flexible, and it is possible to show the
automata, which is important for teaching. If efficiency is needed,
the classifier can be translated into a C++ source, which can be translated
without the library.
The second part is a parser generator. It creates a
runnable parser from the description of a grammar with added action
code. Grammar rules are applied from right to left, and
when a grammar rule is applied, the corresponding action
code is executed. The action code compute the meaning of the recognized
input part. The constructed parser is bottom-up. I think that bottom-up parsing
is better than top-down parsing, because it allows more
grammars, and one can think about the grammar purely as grammar,
not as as something procedural where order of trying matters.
There exist other parser generators that work with C,
but Maphoon fully supports RAII and moving, allows run-time definition of
operators, and has tunable error reporting.
For details, slides, and the sources, I refer to
my site on compiler tools.
A Recursive Inclusion Checker for Recursively Defined Subtypes
My long term goal is to develop a programming that is suitable for
implementation of logic, and maybe also for other domains,
like computer algebra.
Logic is special, because it uses recursively defined datastructures
with many heterogeneous constructors. The algorithms that operate
on these data have
to decide which constructor was used, and after that,
access substructures whose existence depends
on the constructor used.
I argue that that logic reveals a general problem of existing
programming languages:
We do not yet know how to handle type union and partiality in
programming languages, and
how to combine it with static type checking.
Standard programming languages use dynamic dispatch,
enumeration types, pointer casts, variants, or union types.
Logicians traditionally prefer matching, but matching
also flexibility because cases cannot be regrouped.
Instead of these standard approaches,
I propose to handle union by case analysis
on recursively defined subtypes, combined with static type checking
based on these recursively defined subtypes.
In the current talk, I discuss a part of the static
type checking
procedure, namely
a procedure that decides inclusions between recursively
defined subtypes.
The procedure is tableaux-based and uses blocking,
so that termination is guarateed.
The talk was given at Instytut Informatyki in Wrocław.
These are the slides.
(A talk with very similar content was given at
PSSV 2021
in November 2021 in Kazan/Novosibirsk.)
2019
An Easy, Almost Functional Language for Logicians
After several attempts to implement the logic with partial functions
mentioned below in different programming languages, I got tired of
all of them and decided to propose
an own programming language specialized for implementation of logic.
At the time of giving this talk, I had many ideas but no results.
This is the abstract, and
these are the slides.
2019
An Easy, Almost Functional Language for Logicians
After several attempts to implement the logic with partial functions
mentioned below in different programming languages, I got tired of
all of them and decided to propose
an own programming language specialized for implementation of logic.
At the moment of giving this talk, I had many good ideas but no results.
The talk was given at Instytut Informatyki in Wrocław.
This is the abstract, and
these are the slides.
2017
Integrating Logic with Partial Functions into a Proof Checker
I propose a way of integrating Partial Classical Logic
into a proof checker that uses higher-order logic.
This is the abstract, and
these are the slides.
This presentation was given in Dagstuhl.
Solving Satisfiability
Talk at ZOSIA 2017 (Przesieka)
Slides.
The following problem is well-known to be NP-hard:
"Given a set of propositional clauses C, find an interpretation
that makes all clasues in C true".
Despite its NP-hardness, modern implementations are able to
solve large instances in short time. Other search problems
can be solved efficiently by translation them to SAT.
I explain the modern approach to SAT-solving, and demonstrate
use of MiniSat.
Because of its fundamental nature, and the fact that
there exist efficient implementations, I think that
SAT-solving should be part of the standard curriculum.
2013
Theorem Proving in Logic with Partial Functions
Talk at ZJP (Group of Programming Languages) in Wrocław.
Slides,
abstract.
2010
Extending Classical Logic with Partial Functions
Talk was at the Kurt Goedel Colloquium, Technical University
of Vienna on 10.03.2010.
We give a natural semantics for classical logic
with partial functions (PCL).
The semantics is based on multi-valued logic, so that
formulas involving undefined values can have undefined
truth values. An unusual aspect of our semantics is that
it relies on the order of the formulas in a theory.
The semantics is able to capture the fact that
functions and predicates must be declared before they are used.
We think that our approach to partial functions is more
natural than existing approaches, because in our approach,
formulas involving undefined values are guaranteed to be
undefined. In this way, PCL has the same strictness of simple
type theory, while at the same time being much more expressive.
Slides as pdf
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.
Download as 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?
Download as 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.
Download as 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.
Download as 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.
Download as
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 as 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 as 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.
Download as
pdf.
2003
Deciding Modal Logics through Relational Translations into GF2
The talk was given at the M4M workshop in Nancy in September 2003.
It talk is based on a joint paper with Stephane Demri.
Download as pdf.
Translation of Resolution Proofs into Short First-Order Axioms
without Choice Axioms
Talk was given in Dagstuhl, april 2003.
Download as 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.
Download as pdf.
2001
Splitting through new Proposition Symbols
The talk was given at LPAR 2001 in Havana.
Download as pdf.
Translation from S4 into the guarded fragment and the
2-variable fragment
The talk was given in Amsterdam in April 2001.
Download as pdf.
2000
A resolution based decision procedure for the 2-variable
fragment.
Download as pdf.
General Lecture on Resolution Based Theorem Proving
Download as pdf.
1999
Implementation of Resolution
The talk was given in Amsterdam in Mai 1999.
Download as pdf.