- Combining Hilbert Style and Semantic Reasoning in a Resolution Framework
- Elimination of Self-Resolving Clauses
- A Note on Assumptions about Skolem Functions
- Quantifier Elimination in Second--Order Predicate Logic
- Handbook of Logic in AI and Logic Programming: Deduction Systems Based on Resolution
- Reduction Rules for Resolution Based Systems
- The Markgraf Karl Refutation Procedure
- Abstraction Tree Indexing for Terms
- Compilation of Recursive Two-Literal Clauses into Unification Algorithms

**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*

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*

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*

uncompressed files | dvi ( 78K) | PostScript (216K) | PDF (151K) | bib |

compressed files | dvi ( 32K) | PostScript ( 82K) | PDF (135K) |

- the logic, which establishes a notion of semantic entailment;
- the calculus, whose rules of inference provide the syntactic counterpart of entailment;
- the logical state transition system, which determines the representation of formulae or sets of formulae together with their interrelationships, and also may allow additional operations reducing the search space;
- the control, which comprises the criteria used to choose the most promising from among all applicable inference steps.

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.

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*

uncompressed files | PostScript (668K) | PDF (207K) | bib |

compressed files | PostScript (170K) | PDF (184K |

**Abstraction Tree Indexing for Terms**

*Hans Jürgen Ohlbach*

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*

uncompressed files | PostScript (255K) | PDF ( 49K) | bib |

compressed files | PostScript ( 49K) | PDF ( 45K) |