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 is accepted at IJCAR 2016. A preprint is available here. I also gave talk at our local seminar about this topic.

The paper has been accepted for publication in the Journal of Logic and Computation. This is a preprint.

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.

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.

- 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 or ps.gz . 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 thesis as pdf or ps .

Download paper as pdf or ps.gz . The paper was published at CSL 94.