Peter Baumgartner and Michael Kühn.
Abductive Coreference by Model Construction.
In ICoS-1 Inference in Computational Semantics, Institute for Logic, Language and Computation, University of Amsterdam, August 1999. [ bib | .ps.gz ]
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].

 
Peter Baumgartner, Norbert Eisinger, and Ulrich Furbach.
A Confluent Connection Calculus.
In Ganzinger [7], pages 329-343. [ bib | .ps.gz ]
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.

 
Peter Baumgartner, J.D. Horton, and Bruce Spencer.
Merge Path Improvements for Minimal Model Hyper Tableaux.
In Murray [6]. [ bib | .ps.gz ]
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.

 
Peter Baumgartner and Dorothea Schäfer.
Model Elimination with Simplification and its Application to Software Verification.
In Rudolf Berghammer and Yassine Lakhnech, editors, Tool Support for System Specification, Development, and Verification, Advances in Computer Science. Springer-Verlag Wien NewYork, 1999. [ bib | .pdf ]
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.

 
Peter Baumgartner, Norbert Eisinger, and Ulrich Furbach.
A Confluent Connection Calculus.
In Steffen Hölldobler, editor, Intellectics and Computational Logic - Papers in Honor of Wolfgang Bibel. Kluwer, 1999. [ bib | .ps.gz ]
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.

 
Neil Murray, editor.
Automated Reasoning with Analytic Tableaux and Related Methods, volume 1617 of Lecture Notes in Artificial Intelligence. Springer, 1999. [ bib ]
 
Harald Ganzinger, editor.
Automated Deduction - CADE-16, volume 1632 of Lecture Notes in Artificial Intelligence, Trento, Italy, 1999. Springer. [ bib ]