peter-1996.bib
@comment{{This file has been generated by bib2bib 1.99}}
@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}. }
}