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