peter-1997.bib
@comment{{This file has been generated by bib2bib 1.99}}
@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}}
@article{Baumgartner:Furbach:Stolzenburg:RestartMEAnswers:AI:97,
author = {Peter Baumgartner and Ulrich Furbach and Frieder
Stolzenburg},
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 = {}
}
@article{Baumgartner:Bruening:MESS:JAR:97,
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
experiments.}
}
@inproceedings{Baumgartner:Furbach:RMERefinements:FTP:97,
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. }
}
@inproceedings{Aravindan:Baumgartner:ViewDeletion:ILPS:97,
author = {Chandrabose Aravindan and Peter Baumgartner},
title = {{A Rational and Efficient Algorithm for View Deletion in
Databases}},
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.}
}
@inproceedings{Baumgartner:Furbach:CalculiForDLP:ILPS:97,
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.}
}
@inproceedings{Baumgartner:etal:TableauxDiagnosis:IJCAI:97,
author = {Peter Baumgartner and Peter Fr{\"o}hlich and Ulrich
Furbach and Wolfgang Nejdl},
title = {{Semantically Guided Theorem Proving for Diagnosis
Applications}},
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.}
}
@inproceedings{Baumgartner:etal:TableauxDiagnosis:Tableaux:97,
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
applications.}
}
@inproceedings{Baumgartner:Furbach:Stolzenburg:RestartMEAnswers:IJCAI:95,
author = {Peter Baumgartner and Ulrich Furbach and Frieder
Stolzenburg},
title = {{Model Elimination, Logic Programming and Computing
Answers}},
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. }
}
@techreport{baumgartner:23:97,
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 = {http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-23-97.ps.gz},
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.}
}
@proceedings{TABLEAUX:97,
booktitle = {Automated Reasoning with Analytic Tableaux and Related
Methods},
title = {Automated Reasoning with Analytic Tableaux and Related
Methods},
year = {1997},
editor = {Didier Galmiche},
publisher = {Springer},
volume = {1227},
series = {Lecture Notes in Artificial Intelligence},
optannote = { }
}
@proceedings{IJCAI:95,
booktitle = {14th International Joint Conference on Artificial
Intelligence (IJCAI 95)},
year = {1997},
publisher = {Morgan Kaufmann},
address = {Montreal}
}
@proceedings{IJCAI:97,
booktitle = {15th International Joint Conference on Artificial
Intelligence (IJCAI 97)},
editor = {M. E. Pollack},
year = {1997},
publisher = {Morgan Kaufmann},
address = {Nagoya}
}
@proceedings{ILPS:97,
booktitle = {Logic Programming - Proceedings of the 1997 International
Symposium},
editor = {Jan Maluszynski},
year = {1997},
publisher = {The MIT Press},
title = {Logic Programming - Proceedings of the 1997 International
Symposium},
address = {Port Jefferson, New York}
}