@comment{{This file has been generated by bib2bib 1.95}}
@comment{{Command line: bib2bib -c 'year=1997 and not annote:"skip_html" and not annote:"unpublished"' -ob peter-1997.bib -oc peter-1997.cite peter.bib}}
  author = {Peter Baumgartner and Ulrich Furbach and Frieder
  title = {{Computing Answers with Model Elimination}},
  optcrossref = {},
  optkey = {},
  journal = {Artificial Intelligence},
  year = {1997},
  volume = {90},
  era = {A*},
  number = {1--2},
  pages = {135--176},
  url = {answers.pdf},
  abstract = {We demonstrate that theorem provers using model
		  elimination (ME) can be used as answer-complete
		  interpreters for {\em disjunctive logic programming\/}.
		  More specifically, we introduce a family of restart
		  variants of model elimination, and we introduce a mechanism
		  for computing answers. Building on this, we develop a new
		  calculus called {\em ancestry restart ME\/}. This variant
		  admits a more restrictive regularity restriction than
		  restart ME, and, as a side effect, it is in particular
		  attractive for computing definite answers. The presented
		  calculi can also be used successfully in the context of
		  {\em automated theorem proving}. We demonstrate
		  experimentally that it is more difficult to compute
		  non-trivial answers to goals than to prove the {\em
		  existence} of answers.},
  optmonth = {},
  optannote = {}
  author = {Peter Baumgartner and Stefan Br{\"u}ning},
  title = {{A Disjunctive Positive Refinement of Model Elimination
		  and its Application to Subsumption Deletion}},
  journal = {Journal of Automated Reasoning},
  volume = {19},
  era = {A},
  number = {2},
  pages = {205--262},
  year = {1997},
  url = {RR-6-95.pdf},
  abstract = {The Model Elimination (ME) calculus is a refutationally
		  complete, goal-oriented calculus for first-order clause
		  logic. In this paper, we introduce a new variant called
		  {\em disjunctive positive ME (DPME)\/}; it improves on
		  Plaisted's positive refinement of ME in that reduction
		  steps are allowed only with positive literals stemming from
		  clauses having at least two positive literals (so-called
		  {\em disjunctive\/} clauses). \par DPME is motivated by its
		  application to various kinds of {\em subsumption\/}
		  deletion: in order to apply subsumption deletion in ME
		  equally successful as in Resolution, it is crucial to
		  employ a version of ME which minimizes ancestor context
		  (i.e.\ the necessary A-literals to find a refutation). DPME
		  meets this demand. We describe several variants of ME with
		  subsumption, with the most important ones being {\em ME
		  with backward and forward subsumption\/} and the {\em
		  T$^{*}$-Context Check\/}. We compare their pruning power,
		  also taking into consideration the well-known regularity
		  restriction. \par All proofs are supplied. The
		  practicability of our approach is demonstrated with
  author = {Peter Baumgartner and Ulrich Furbach},
  title = {{Refinements for Restart Model Elimination}},
  url = {refinements-for-restart-model.pdf},
  booktitle = {Proceedings of the International Workshop on First Order
		  Theorem Proving (FTP 97)},
  era = {B},
  series = {Technical Report},
  publisher = {RISC-Linz},
  year = {1997},
  month = oct,
  optnumber = {},
  optvolume = {},
  abstract = { We introduce and discuss a number of refinements for
		  restart model elimination (RME). Most of these refinements
		  are motivated by the use of RME as an interpreter for
		  disjunctive logic programming. Especially head selection
		  function, computation rule, strictness and independence of
		  the goal clause are motivated by aiming at a procedural
		  interpretation of clauses. Other refinements like
		  regularity and early cancellation pruning are techniques to
		  handle the tremendous search space. We discuss these
		  techniques and investigate their compatibility. As a new
		  result we give a proof of completeness for RME with early
		  cancellation pruning; we furthermore show that this
		  powerful refinement is compatibel with regularity tests. }
  author = {Chandrabose Aravindan and Peter Baumgartner},
  title = {{A Rational and Efficient Algorithm for View Deletion in
  crossref = {ILPS:97},
  url = {dbu.pdf},
  abstract = { In this paper, we show how techniques from disjunctive
		  logic programming and classical first-order theorem proving
		  can be used for efficient (deductive) database updates. The
		  key idea is to tranform the given database together with
		  the update request into a disjunctive logic program and
		  apply disjunctive techniques (such as minimal model
		  reasoning) to solve the original update problem. We present
		  two variants of our algorithm both of which are of
		  polynomial space complexity. One variant, which is based on
		  offline preprocessing, is of polynomial time complexity. We
		  also show that both variants are rational in the sense that
		  they satisfy certain rationality postulates stemming from
		  philosophical works on belief dynamics.}
  author = {Peter Baumgartner and Ulrich Furbach},
  title = {{Calculi for Disjunctive Logic Programming}},
  url = {ilps97-proceedings.pdf},
  crossref = {ILPS:97},
  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.}
  author = {Peter Baumgartner and Peter Fr{\"o}hlich and Ulrich
		  Furbach and Wolfgang Nejdl},
  title = {{Semantically Guided Theorem Proving for Diagnosis
  url = {baumgartner97semantically.pdf},
  era = {A},
  crossref = {IJCAI:97},
  pages = {460--465},
  abstract = { In this paper we demonstrate how general purpose
		  automated theorem proving techniques can be used to solve
		  realistic model-based diagnosis problems. For this we
		  modify a model generating tableau calculus such that a
		  model of a correctly behaving device can be used to guide
		  the search for minimal diagnoses. Our experiments show that
		  our general approach is competitive with specialized
		  diagnosis systems.}
  author = {Peter Baumgartner and Peter Fr{\"o}hlich and Ulrich
		  Furbach and Wolfgang Nejdl},
  title = {{Tableaux for Diagnosis Applications}},
  crossref = {TABLEAUX:97},
  url = {baumgartner96tableaux.pdf},
  era = {A},
  pages = {76--90},
  abstract = {In \cite{nej96} a very efficient system for solving
		  diagnosis tasks has been described, which is based on
		  belief revision procedures and uses first order logic
		  system descriptions. In this paper we demonstrate how such
		  a system can be rigorously formalized from the viewpoint of
		  deduction by using the calculus of hyper tableaux
		  \cite{Baumgartner:etal:HyperTableau:JELIA:96}. The benefits
		  of this approach are twofold: first, it gives us a clear
		  logical description of the diagnosis task to be solved;
		  second, as our experiments show, the approach is feasible
		  in practice and thus serves as an example of a successful
		  application of deduction techniques to real-world
  author = {Peter Baumgartner and Ulrich Furbach and Frieder
  title = {{Model Elimination, Logic Programming and Computing
  crossref = {IJCAI:95},
  volume = {1},
  era = {A},
  pages = {335--340},
  url = {ijcai-me+ans.pdf},
  abstract = {We prove that theorem provers using model elimination (ME)
		  can be used as answer complete interpreters for {\em
		  disjunctive logic programming\/}. For this, the restart
		  variant of ME with a mechanism for computing answers and
		  the ancestry refinement is introduced. Furthermore, we
		  demonstrate that in the context of {\em automated theorem
		  proving\/} it is much more difficult to compute
		  (non-trivial) answers to goals, instead of only proving the
		  {\em existence\/} of answers. It holds that resolution with
		  subsumption is {\em not\/} answer complete. We consider
		  puzzle examples and give a comparative study of OTTER,
		  SETHEO and our restart model elimination prover PROTEIN. }
  author = {Peter {Baumgartner~(Hrsg.)}},
  title = {{Jahrestreffen der GI-Fachgruppe 1.2.1 `Deduktionssysteme'
		  --- Kurzfassungen der Vortr{\"a}ge}},
  institution = {Universit{\"a}t Koblenz-Landau},
  year = {1997},
  type = {Fachberichte Informatik},
  number = {23--97},
  language = {german},
  address = {Universit{\"a}t Koblenz-Landau, Institut f{\"u}r
		  Informatik, Rheinau 1, D-56075 Koblenz},
  url = {},
  abstract = {Das Jahrestreffen 1997 der GI-Fachgruppe 1.2.1
		  `Deduktionssysteme' --- besser bekannt als
		  `Deduktionstreffen' --- fand vom 30.9.\ bis 2.10.\ 1997 in
		  Schloss Dagstuhl statt. Die Organisation wurde dieses Jahr
		  von der KI-Gruppe an der Universit{\"a}t Koblenz-Landau
		  (Leitung Prof.~Furbach) {{\"u}}bernommen.}
  booktitle = {Automated Reasoning with Analytic Tableaux and Related
  title = {Automated Reasoning with Analytic Tableaux and Related
  year = {1997},
  editor = {Didier Galmiche},
  publisher = {Springer},
  volume = {1227},
  series = {Lecture Notes in Artificial Intelligence},
  optannote = { }
  booktitle = {14th International Joint Conference on Artificial
		  Intelligence (IJCAI 95)},
  year = {1997},
  publisher = {Morgan Kaufmann},
  address = {Montreal}
  booktitle = {15th International Joint Conference on Artificial
		  Intelligence (IJCAI 97)},
  editor = {M. E. Pollack},
  year = {1997},
  publisher = {Morgan Kaufmann},
  address = {Nagoya}
  booktitle = {Logic Programming - Proceedings of the 1997 International
  editor = {Jan Maluszynski},
  year = {1997},
  publisher = {The MIT Press},
  title = {Logic Programming - Proceedings of the 1997 International
  address = {Port Jefferson, New York}