@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}}
  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 = {}
  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}
  author = {Peter Baumgartner and Ulrich Furbach and Ilkka
  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.}
  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 = {}
  optcrossref = {},
  optkey = {},
  author = {Peter Baumgartner and Ulrich Furbach},
  title = {{Hyper Tableaux. Part I: Proof Procedure and Model
  howpublished = {Dagstuhl-Seminar Reports {\em Disjunctive logic
		  programming and databases: Non-monotonic aspects\/}},
  year = {1996},
  optmonth = {},
  optnote = {},
  optannote = {}
  author = {Peter Baumgartner and Ulrich Furbach},
  title = {{Hyper Tableaux and Disjunctive Logic Programming}},
  booktitle = {ICLP 96 Workshop on Deductive Databases and Logic
  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.}
  optcrossref = {},
  optkey = {},
  author = {Artificial Intelligence Research Group},
  title = {{Towards Merging Theorem Proving and Logic Programming
  howpublished = {Proc. of the Poster Session at JICSLP '96, Editors: N.
		  Fuchs and U. Geske},
  year = {1996},
  optmonth = {},
  note = {GMD Studien Nr. 296},
  optannote = {}
  author = {Peter Baumgartner and Bernhard Beckert and Michael
  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}. }