Dr. Hans Jürgen Ohlbach

Selected Publications about Theorem Proving in Predicate Logic

Combining Hilbert Style and Semantic Reasoning in a Resolution Framework
Hans Jürgen Ohlbach

Abstract:
Many non-classical logics can be axiomatized by means of Hilbert Systems. Reasoning in Hilbert Systems, however, is extremely inefficient. Most inference methods therefore use the semantics of a logic in one kind or another to get more efficiency. In this paper a combination of Hilbert style and semantic reasoning is proposed. It is particularly tailored for cases where either the semantics of some operators is not known, or it is second-order, or it is just too complicated to handle, or flexibility in experimenting with different versions of a logic is required. First-order predicate logic is used as a meta-logic for combining the Hilbert part with the semantics part. Reasoning is done in a (theory) resolution framework.

The basic method is applicable to many different (monotonic propositional) non-classical logics. It can, however, be improved by treating particular formulae in a special way, as rewrite rules, as theory unification or theory resolution rules, even as recursive calls to a theorem prover. Examples for all these cases are presented in the paper.

Download
uncompressed files dvi ( 58K) PostScript (186K) PDF (134K) bib
compressed files dvi ( 23K) PostScript ( 71K) PDF (118K)

Elimination of Self-Resolving Clauses
Hans Jürgen Ohlbach

Abstract:
It is shown how self-resolving clauses like symmetry or transitivity, or even clauses like condensed detachment, can faithfully be deleted from the clause set thus eliminating or at least reducing recursiveness and circularity in clause sets. Possible applications are reducing the search space for automated theorem provers, eliminating loops in Prolog programs, parallelizing simple closure computation algorithms and supporting automated complexity analysis.

Download
uncompressed files dvi ( 77K) PostScript (282K) PDF (167K) bib
compressed files dvi ( 30K) PostScript (101K) PDF (144K)

A Note on Assumptions about Skolem Functions
Hans Jürgen Ohlbach and Christoph Weidenbach

Abstract:
Skolemization is not an equivalence preserving transformation. For the purposes of refutational theorem proving it is sufficient that Skolemization preserves satisfiability and unsatisfiability. Therefore there is sometimes some freedom in interpreting Skolem functions in a particular way. We show that in certain cases it is possible to exploit this freedom for simplifying formulae considerably. Examples for cases where this occurs systematically are the relational translation from modal logics to predicate logic and the relativization of first-order logics with sorts.

Download
uncompressed files dvi ( 34K) PostScript (141K) PDF ( 94K) bib
compressed files dvi ( 13K) PostScript ( 55K) PDF ( 82K)

Quantifier Elimination in Second--Order Predicate Logic
Dov Gabbay and Hans Jürgen Ohlbach

Abstract:
An algorithm is presented which eliminates second--order quantifiers over predicate variables in formulae of type exists P1,...,PnF where F is an arbitrary formula of first--order predicate logic. The resulting formula is equivalent to the original formula -- if the algorithm terminates. The algorithm can for example be applied to do interpolation, to eliminate the second--order quantifiers in circumscription, to compute the correlations between structures and power structures, to compute semantic properties corresponding to Hilbert axioms in non classical logics and to compute model theoretic semantics for new logics.

Download
uncompressed files dvi ( 78K) PostScript (216K) PDF (151K) bib
compressed files dvi ( 32K) PostScript ( 82K) PDF (135K)

Handbook of Logic in AI and Logic Programming: Deduction Systems Based on Resolution
Norbert Eisinger and Hans Jürgen Ohlbach

Abstract:
A general theory of deduction systems is presented. The theory is illustrated with deduction systems based on the resolution calculus, in particular with clause graphs. This theory distinguishes four constituents of a deduction system:

Much of the standard material on resolution is presented in this framework. For the last two levels many alternatives are discussed. Apropriately adjusted notions of soundness, completeness, confluence, and Noetherianness are introduced in order to characterize the properties of particular deduction systems. For more complex deduction systems, where logical and topological phenomena interleave, such properties can be far from obvious.

Download PDF (604K)

Reduction Rules for Resolution Based Systems
Norbert Eisinger, Hans Jürgen Ohlbach and Axel Präcklein

Abstract:
Inference rules for resolution based systems can be classified into deduction rules, which add new objects, and reduction rules, which remove objects. Traditional reduction rules like subsumption do not actively contribute to a solution, but they help to avoid redundancies in the search space. We present a number of advanced reduction rules, which can cope with high degrees of redundancy and play a distinctly active part because they find trivial solutions on their own and thus relieve the control component for the deduction rules from low level tasks. We describe how these reduction rules can be implemented with reasonable efficiency in a clause graph resolution system, but they are not restricted to this particular representation.

Download
uncompressed files PostScript (349K) PDF (105K) bib
compressed files PostScript ( 84K) PDF ( 89K)

The Markgraf Karl Refutation Procedure
Hans Jürgen Ohlbach and Jörg H. Siekmann

Abstract:
The goal of the {\em MKRP project} is the development of a theorem prover which can be used as an inference engine in various applications, in particular it should be capable of proving significant mathematical theorems. Our first implementation, the {\em Markgraf Karl Refutation Procedure (MKRP)} realizes some of the ideas we have developed to this end. It is a general purpose resolution based deduction system that exploits the representation of formulae as a graph (clause graph). The main features are its well tailored selection components, heuristics and control mechanisms for guiding the search for a proof.

This paper gives an overview of the system. It summarizes and evaluates our experience with the system in particular, and the logics we use as well as the clause graph approach: as 1990 marks the fifteenth birthday of the system, the time may have come to ask: ``Was it worth the effort?''

Download
uncompressed files PostScript (668K) PDF (207K) bib
compressed files PostScript (170K) PDF (184K

Abstraction Tree Indexing for Terms
Hans Jürgen Ohlbach

Abstract:
An indexing technique for first-order predicate logic terms and literals is proposed. It exploits the lattice structure of terms, generated by the usual instance relation, to provide for a given ``query term'' fast access to all T-unifiable terms, T-instances (backward subsumption) and T-generalized terms (forward subsumption) where T is any finitary unification theory. In the best case one single unification or matching operation respectively is sufficient to access a large number of unifiable terms or instances at once.

Download
uncompressed files PostScript (188K) PDF ( 38K) bib
compressed files PostScript ( 46K) PDF ( 34K)

Compilation of Recursive Two-Literal Clauses into Unification Algorithms
Hans Jürgen Ohlbach

Abstract:
Automated deduction systems can considerably be improved by replacing axioms with special purpose inference mechanisms. For example replacing in resolution based systems certain equations with theory unification algorithms reduces the amount of search because the algorithm introduces more determinism in the otherwise blind search strategy. Non-recursive clauses with two literals, i.e. clauses which do not resolve with a copy of themselves can be compiled automatically into a unification algorithm for literals which realizes a theory resolution with respect to the theory of the compiled clause. In this paper the compilation technique is extended to arbitrary clauses with two literals. The technique uses so called abstraction trees with continuations to represent potentially infinitely many self resolvents. These trees allow to detect easily how many copies of the compiled clause are necessary to (theory-) resolve two other clauses.

Download
uncompressed files PostScript (255K) PDF ( 49K) bib
compressed files PostScript ( 49K) PDF ( 45K)

Last Modified: Monday, 20-Mar-2006 10:58:06 CET