@comment{{This file has been generated by bib2bib 1.95}}

@comment{{Command line: bib2bib -c 'year=1996 and not annote:"skip_html" and not annote:"unpublished"' -ob peter-1996.bib -oc peter-1996.cite peter.bib}}

@article{Baumgartner:LinearizingCompletion:JAR:96, author = {Peter Baumgartner}, title = {{Linear and Unit-Resulting Refutations for Horn Theories}}, optcrossref = {}, optkey = {}, era = {A}, journal = {Journal of Automated Reasoning}, year = {1996}, volume = {16}, number = {3}, pages = {241--319}, month = {June}, url = {lincomp.pdf}, abstract = {We present a new transformation method by which a given Horn theory is transformed in such a way that resolution derivations can be carried out which are both linear (in the sense of Prologs SLD-resolution) {\em and\/} unit-resulting (i.e.\ the resolvents are unit clauses). This is not trivial since although both strategies alone are complete, their na{{\"\i}}{}ve combination is not. Completeness is recovered by our method through a completion procedure in the spirit of Knuth-Bendix completion, however with different ordering criteria. A powerful redundancy criterion helps to find a finite system quite often. \\ The transformed theory can be used in combination with linear calculi such as e.g.\ (theory) model elimination to yield sound, complete and efficient calculi for full first order clause logic over the given Horn theory. \\ As an example application, our method discovers a generalization of the well-known linear paramodulation calculus for the combined theory of equality and strict orderings. \\ The method has been implemented and has been tested in conjunction with a model elimination theorem prover.}, optnote = {}, optannote = {} }

@article{Baumgartner:etal:DeduktionUndLP:KI:96, author = {Peter Baumgartner and J{\"u}rgen Dix and Ulrich Furbach and Dorothea Sch{\"a}fer and Frieder Stolzenburg}, title = {{Deduktion und Logisches Programmieren}}, journal = {KI}, year = 1996, volume = 10, number = 2, pages = {34-39} }

@inproceedings{Baumgartner:Furbach:Niemelae:HyperTableau:JELIA:96, author = {Peter Baumgartner and Ulrich Furbach and Ilkka Niemel{\"a}}, title = {{Hyper Tableaux}}, optcrossref = {}, optkey = {}, opteditor = {}, optvolume = {}, number = {1126}, era = {A}, series = {Lecture Notes in Artificial Intelligence}, optpages = {}, booktitle = {Logics in Artificial Intelligence (JELIA '96)}, year = {1996}, publisher = {Springer}, optaddress = {}, optmonth = {}, optannote = {}, url = {tableaux-jelia-llncs.pdf}, abstract = { This paper introduces a variant of clausal normal form tableaux that we call ``hyper tableaux''. Hyper tableaux keep many desirable features of analytic tableaux while taking advantage of the central idea from (positive) hyper resolution, namely to resolve away all negative literals of a clause in a single inference step. Another feature of the proposed calculus is the extensive use of universally quantified variables. This enables new efficient forward-chaining proof procedures for full first order theories as variants of tableaux calculi.} }

@phdthesis{Baumgartner:TheoryReasoning:PhDThesis:96, author = {Peter Baumgartner}, title = {{Theory Reasoning in Connection Calculi and the Linearizing Completion Approach}}, school = {Universit{\"a}t Koblenz-Landau}, year = {1996}, url = {diss-baumgartner.pdf}, optcrossref = {}, optkey = {}, optaddress = {}, optmonth = {}, opttype = {}, abstract = {This thesis is on extensions of calculi for automated theorem proving towards theory reasoning. It focuses on connection methods\index{Connection!Method} and in particular on theory model elimination (TME). For TME the emphasis lies on the combination with theory reasoners to be obtained by new compilation approach. \par Several theory-reasoning versions of connection calculi are defined and related to each other. In doing so, TME will be selected as a base to be developed further. The final versions are search-space restricted versions of total TME, partial TME and partial restart TME. These versions all are {\em answer\/}-complete, thus making TME interesting for logic programming and problem-solving applications. \par A theory reasoning system is only operable in combination with an (efficient) background reasoner for the theories of interest. Instead of hand-crafting respective background reasoners, a more general approach --- linearizing completion --- is proposed. Linearizing completion enables the {\em automatic\/} construction of background calculi suitable for TME-based theory reasoning systems from a wide range of axiomatically given theories, namely Horn theories. \par Technically, linearizing completion is a device for combining the unit-resulting strategy of resolution with a goal-oriented, linear strategy {\`a} la Prolog in a refutationally complete way. The method is presented in detail. \par Finally, an implementation extending the PTTP technique (Prolog based Technology Theorem Proving) towards theory reasoning is described, and the usefulness of the methods developed in this text will be experimentally demonstrated.}, optannote = {} }

@misc{Baumgartner:Furbach:HyperTableaux:Dagstuhl:96, optcrossref = {}, optkey = {}, author = {Peter Baumgartner and Ulrich Furbach}, title = {{Hyper Tableaux. Part I: Proof Procedure and Model Generation}}, howpublished = {Dagstuhl-Seminar Reports {\em Disjunctive logic programming and databases: Non-monotonic aspects\/}}, year = {1996}, optmonth = {}, optnote = {}, optannote = {} }

@incollection{Baumgartner:Furbach:HyperTableauxAndDLP:DDLP:96, author = {Peter Baumgartner and Ulrich Furbach}, title = {{Hyper Tableaux and Disjunctive Logic Programming}}, booktitle = {ICLP 96 Workshop on Deductive Databases and Logic Programming}, howpublished = {Workshop Deductive Databases and Logic Programming (DD\&LP'96) at {\em Joint International Conference and Symposium on Logic Programming\/}}, year = {1996}, url = {fix-jicslp96.pdf}, publisher = {GMD}, opteditor = {}, volume = {295}, optnumber = {}, series = {GMD Studien}, abstract = { We introduce a bottom-up and a top-down calculus for disjunctive logic programming (DLP). The bottom-up calculus, hyper tableaux, is depicted in its ground version and its relation to fixed point approaches from the literature is investigated. The top-down calculus, restart model elimination (RME), is presented as a sound and complete answer-computing mechanism for DLPs, and its relation to hyper tableaux is discussed. \\ In two aspect this represents an extension of SLD-resolution for Horn clause logic programming: RME {\em is\/} SLD-resolution when restricted to Horn clauses, and it has a direct counterpart to the immediate consequence operator for Horn clauses. Furthermore we discuss, that hyper tableaux can be seen as an extension of SLO-resolution.} }

@misc{AIGROUP:MergingTPandLP:Poster:JICSLP:96, optcrossref = {}, optkey = {}, author = {Artificial Intelligence Research Group}, title = {{Towards Merging Theorem Proving and Logic Programming Paradigms}}, howpublished = {Proc. of the Poster Session at JICSLP '96, Editors: N. Fuchs and U. Geske}, year = {1996}, optmonth = {}, note = {GMD Studien Nr. 296}, optannote = {} }

@inproceedings{Baumgartner:Kuehn:Beckert:EHyperTableaux:DeduktionWS:96, author = {Peter Baumgartner and Bernhard Beckert and Michael K{\"u}hn}, title = {{Extending Hyper Tableaux with Rigid $E$-Unification}}, editor = {K. Prasser}, number = {WV-96-09}, series = {Internal Reports}, booktitle = {Workshop Deduktion, 20.\ Jahrestagung f{\"u}r k{\"u}nstliche Intelligenz, Zusammenfassungen}, year = 1996, organization = {Technische Universit{\"a}t Dresden}, address = {Fakult{\"a}t Informatik, D01062 Dresden}, url = {tableaux-dedtreff96.pdf}, abstract = {In \cite{Baumgartner:etal:HyperTableau:JELIA:96} we introduced a variant of clausal normal form tableaux called ``hyper tab\-leaux''. In the talk we well report about ongoing work on two improvements of the basic calculus. The first improvement deals with a shortcoming of the basic calculus, which is the need for ``purifying'' substitutions in disjunctions of positive literals. The second improvement is the extension with a dedicated inference rule for equality. We will use the completion-based method for mixed universal and rigid $E$-unification of \cite{Beckert:MixedUnification:94}. } }