In this paper, we argue that the resolution of anaphoric expressions in an utterance is essentially an abductive task following [HSAM93] who use a weighted abduction scheme on horn clauses to deal with reference. We give a semantic representation for utterances containing anaphora that enables us to compute possible antecedents by abductive inference. We extend the disjunctive model construction procedure of hyper tableaux [BFN96, Küh97] with a clause transformation turning the abductive task into a model generation problem and show the completeness of this transformation with respect to the computation of abuctive explanations. This abductive inference is applied to the resolution of anaphoric expressions in our general model constructing framework for incremental discourse representation [Küh99] which we argue to be useful for computing information updates from natural language utterances [Vel96].

This work is concerned with basic issues of the design of calculi and proof procedures for first-order connection methods and tableaux calculi. Proof procedures for these type of calculi developed so far suffer from not exploiting proof confluence, and very often unnecessarily rely on a heavily backtrack oriented control regime.

As a new result, we present a variant of a connection calculus and prove its strong completeness. This enables the design of backtrack-free control regimes. To demonstrate that the underlying fairness condition is reasonably implementable we define an effective search strategy. We show that with the new approach the search space can be exponentially smaller than those of current, backtracking-oriented proof procedures based on weak completeness results.

This paper describes our approach of coupling the interactive software verification system KIV with the Model Elimination based, complete automated theorem prover PROTEIN. In order to make this combination work in practice, we propose to incorporate domain knowledge readily given from the KIV domain into PROTEIN. More specifically, we extend Model Elimination by a concept of simplification based on conditional rewrite rules. The extension is defined in such a way that rewrite rules as given from the KIV system can easily be accommodated. This yields better performance for proof automatization and thus relieves the system engineer from more interactions. In the paper, we describe the new simplification technique, show completeness, and demonstrate the benefits with practical experiments from the KIV domain.

We combine techniques originally developed for refutational first-order theorem proving within the clause tree framework with techniques for minimal model computation developed within the hyper tableau framework. This combination generalizes well-known tableaux techniques like complement splitting and folding-up/down. We argue that this combination allows for efficiency improvements over previous, related methods. It is motivated by application to diagnosis tasks; in particular the problem of avoiding redundancies in the diagnoses of electrical circuits with reconvergent fanouts is addressed by the new technique. In the paper we develop as our main contribution in a more general way a sound and complete calculus for propositional circumscriptive reasoning in the presence of minimized and varying predicates.

This work is concerned with basic issues of the design of calculi and proof procedures for first-order connection methods and tableaux calculi. Proof procedures for these type of calculi developed so far suffer from not exploiting proof confluence, and very often unnecessarily rely on a heavily backtrack oriented control regime.

As a new result, we present a variant of a connection calculus and prove its strong completeness. This enables the design of backtrack-free control regimes. To demonstrate that the underlying fairness condition is reasonably implementable we define an effective search strategy.