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



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 .


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 .


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 .


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 .


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)


On the generation of Proofs from the Clausal Normal Form Transformation

The talk was given at CSL 2002 in Edingburgh, Scotland. ps or pdf .


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.


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

ps or pdf .

General Lecture on Resolution Based Theorem Proving

ps or pdf .


Implementation of Resolution

ps or pdf . The talk was given in Amsterdam in Mai 1999.