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.)


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.


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.


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.


Theorem Proving in Logic with Partial Functions

Talk at ZJP (Group of Programming Languages) in Wrocław. Slides, abstract.


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


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.


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.


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.


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.


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)


On the generation of Proofs from the Clausal Normal Form Transformation

The talk was given at CSL 2002 in Edingburgh, Scotland. Download as pdf.


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.


A resolution based decision procedure for the 2-variable fragment.

Download as pdf.

General Lecture on Resolution Based Theorem Proving

Download as pdf.


Implementation of Resolution

The talk was given in Amsterdam in Mai 1999. Download as pdf.