## SEKI Report

### Refine

#### Keywords

- Knowledge acquisition (3)
- resolution (3)
- Case-Based Reasoning (2)
- Deduction (2)
- HOT (2)
- MOLTKE-Projekt (2)
- Term rewriting systems (2)
- Wissensakquisition (2)
- analogy (2)
- combined systems with sha (2)

98,8

The paper addresses two problems of comprehensible proof presentation, the hierarchically structured presentation at the level of proof methods and different presentation styles of construction proofs. It provides solutions for these problems that can make use of proof plans generated by an automated proof planner.

98,5

Simultaneous quantifier elimination in sequent calculus is an improvement over the well-known skolemization. It allows a lazy handling of instantiations as well as of the order of certain reductions. We prove the soundness of a sequent calculus which incorporates a rule for simultaneous quantifier elimination. The proof is performed by semantical arguments and provides some insights into the dependencies between various formulas in a sequent.

98,4

This paper describes a tableau-based higher-order theorem prover HOT and an application to natural language semantics. In this application, HOT is used to prove equivalences using world knowledge during higher-order unification (HOU). This extended form of HOU is used to compute the licensing conditions for corrections.

98,3

HOT is an automated higher-order theorem prover based on HTE, an extensional higher-order tableaux calculus (Kohlhase 95). The first part of the paper introduces a variant of the calculus which closely corresponds to the proof procedure implemented in HOT. The second part discusses HOT's design that can be characterized as a concurrent Blackboard architecture. We show the usefulness of the implementation by including benchmark results for over one hundred solved problems from logic and set theory.

97,9

In this paper we provide a semantical meta-theory that will support the development of higher-order calculi for automated theorem proving like the corresponding methodology has in first-order logic. To reach this goal, we establish classes of models that adequately characterize the existing theorem-proving calculi, that is, so that they are sound and complete to these calculi, and a standard methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of machine-oriented calculi.

96,10

Planning for realistic problems in a static and deterministic environment with complete information faces exponential search spaces and, more often than not, should produce plans comprehensible for the user. This article introduces new planning strategies inspired by proof planning examples in order to tackle the search-space-problem and the structured-plan-problem. Island planning and refinement as well as subproblem refinement are integrated into a general planning framework and some exemplary control knowledge suitable for proof planning is given.

93,11

This report contains a collection of abstracts for talks given at the "Deduktionstreffen" held at Kaiserslautern, October 6 to 8, 1993. The topics of the talks range from theoretical aspects of term rewriting systems and higher order resolution to descriptions of practical proof systems in various applications. They are grouped together according the following classification: Distribution and Combination of Theorem Provers, Termination, Completion, Functional Programs, Inductive Theorem Proving, Automatic Theorem Proving, Proof Presentation. The Deduktionstreffen is the annual meeting of the Fachgruppe Deduktionssysteme in the Gesellschaft für Informatik (GI), the German association for computer science.

94,3

A method for efficiently handling associativity and commutativity (AC) in implementations of (equational) theorem provers without incorporating AC as an underlying theory will be presented. The key of substantial efficiency gains resides in a more suitable representation of permutation-equations (such as f(x,f(y,z))=f(y,f(z,x)) for instance). By representing these permutation-equations through permutations in the mathematical sense (i.e. bijective func- tions :{1,..,n} {1,..,n}), and by applying adapted and specialized inference rules, we can cope more appropriately with the fact that permutation-equations are playing a particular role. Moreover, a number of restrictions concerning application and generation of permuta- tion-equations can be found that would not be possible in this extent when treating permu- tation-equations just like any other equation. Thus, further improvements in efficiency can be achieved.

98,2

We examine an approach for demand-driven cooperative theorem proving.We briefly point out the problems arising from the use of common success-driven cooperation methods, and we propose the application of our approachof requirement-based cooperative theorem proving. This approach allows for abetter orientation on current needs of provers in comparison with conventional co-operation concepts. We introduce an abstract framework for requirement-basedcooperation and describe two instantiations of it: Requirement-based exchangeof facts and sub-problem division and transfer via requests. Finally, we reporton experimental studies conducted in the areas superposition and unfailing com-pletion.The author was supported by the Deutsche Forschungsgemeinschaft (DFG).