We give the standard algorithms for tokenizer construction with automata, namely construction using regular operations, determinization, and minimization. We 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 is joint work with Dina Muktubayeva.

This paper has been accepted by GandALF 2022. This is a preprint.

This work is part of a project to design a new programming language suitable for efficient implementation of logic. Logical formulas are tree-like structures with many constructors having different arities and argument types. Algorithms that use these structures must perform case analysis on the constructors, and access subtrees whose type and existence depend on the constructor used.

In many programming languages, case analysis is handled by matching, but we want to take a different approach, based on recursively defined subtypes. Instead of matching a tree against different constructors, we will classify it by using a set of disjoint subtypes. Subtypes are more general than structural forms based on constructors, we expect that they can be implemented more efficiently, and in addition can be used in static type checking. This makes it possible to use recursively defined subtypes as preconditions or postconditions of functions.

We define the types and the subtypes (which we will
call *adjectives*), define their semantics,
and give a tableaux-based inclusion checker for adjectives.
We show how to use this inclusion checker for resolving ambiguous field
references in declarations of adjectives. The same procedure
can be used for resolving ambiguous function calls.

This paper will appear in a special issue of Modeling and Analysis of Information Systems dedicated to the 12th workshop on Program Semantics, Specification, and Verification (PSSV 2021). This is a preprint.

The paper appeared in the Journal of Logic and Computation. This is a preprint.

Because matching is not restricted by term structure, matching for geometric resolution is a hard problem. We translate the matching problem into a generalized constraint satisfaction problem, and give an algorithm that solves it efficiently. The algorithm uses learning teachings, similar to clause learning in propositional logic. After that, we adapt the algorithm in such a way that it finds solutions that use a minimal subset of the interpretation.

The techniques presented in this paper may also have applications in constraint solving.

The paper appeared at IJCAR 2016. A preprint is available here. I also gave talk at our local seminar about this topic.

This paper is an extended version of the 2010 IJCAR paper, which was invited to the special issue of IJCAR 2010. This is a preprint of the paper. The final version was published in the Journal of Automated Reasoning, and can be obtained from Springer.

This is a preprint.

Download pdf.

We have studied several aspects related to the use of resolution as decision procedure. The first two papers introduce resolution decision procedures for the guarded fragment with and without equality. The third paper builds on the decision procedure for the guarded fragment. Using the decision procedure, modal logics can be decided by translation into the guarded fragment with the relational translation. We have extended the standard relational translation of modal logics, so that more modal logics can be translated into the guarded fragment. In particular, modal logic S4 can now be translated. Before, only translations into extensions of the guarded fragment existed. The fourth paper shows that a standard refinement of resolution, which uses a liftable order, can be used to obtain a decison procedure for the E-plus class. This was posed as an open problem in (Resolution Methods for the Decision Problem, C. Fermueller, A. Leitsch, T. Tammet, N. Zamov, Springer Verlag 1993)

The fifth paper introduces a resolution-based decision procedure for the two-variable fragment with equality. The procedure consists of three stages: Saturation under resolution, elimination of equality, and one more time saturation under resolution.

Download pdf.

- A clausification procedure in type theory, equipped with a correctness proof, all encoded using higher-order primitive recursion.
- A novel representation of clauses in minimal logic such that the $ \lambda $-representation of resolution steps is linear in the size of the premisses.
- Availability of the power of resolution theorem provers in interactive proof construction systems based on type theory

- How to handle the introduction of definitions and Skolem functions.
- How to generate short (linear size) proofs.
- How to handle optimized Skolemization. We reduce it to standard Skolemization.

Download paper as pdf. The paper was published at CADE 97.

Using Maslov's method, it is very easy to obtain a resolution calculus for every logic that has a cut-free, complete sequent calculus. However, the resolution calculi that are obtained in this way are bottom-up, i.e. working from the axioms towards the goal.

In my thesis, I show that many sequent calculi have a reversal , which is obtained by exchanging axioms and goal, and reversing the direction of the rules. If one applies Maslov's method on the reversed sequent calculus, one obtains a top-down resolution calculus.

Download PhD thesis as pdf.

Download paper as pdf. The paper was published at CSL 94.