peter-2000.bib
@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib -c 'year=2000 and not annote:"skip_html" and not annote:"unpublished"' -ob peter-2000.bib -oc peter-2000.cite peter.bib}}
@article{Baumgartner:Kuehn:AbducingCoreference:JLAC:00,
author = {Peter Baumgartner and Michael K{\"u}hn},
title = {{Abducing Coreference by Model Construction}},
journal = {Journal of Language and Computation},
year = {2000},
volume = {1},
number = {2},
editors = {C. Monz and M. de Rijke},
pages = {175--190},
publisher = {Hermes Science Publishers},
url = {abdcoref-jlac.pdf},
abstract = {In this paper, we argue that the resolution of anaphoric
expressions in an utterance is essentially an
\emph{abductive} task following
\cite{Hobbs:etal:InterpretationAsAbduction:AIJ:93} who use
a weighted abduction scheme on horn clauses to deal with
reference. We give a semantic representation for utterances
containing anaphora that enables us to compute possible
antecedents by abductive inference. We extend the
disjunctive model construction procedure of \emph{hyper
tableaux}
\cite{Baumgartner:Furbach:Niemelae:HyperTableau:JELIA:96,Kuehn:RigidHyperTableaux:KI:97}
with a clause transformation turning the abductive task
into a model generation problem and show the completeness
of this transformation with respect to the computation of
abductive explanations. This abductive inference is applied
to the resolution of anaphoric expressions in our general
model constructing framework for incremental discourse
representation which we argue to be useful for computing
information updates from natural language utterances.}
}
@article{Aravindan:Baumgartner:ViewDeletion:JSC:00,
author = {Chandrabose Aravindan and Peter Baumgartner},
title = {Theorem Proving Techniques for View Deletion in
Databases},
journal = {Journal of Symbolic Computation},
year = {2000},
optkey = {},
volume = {29},
number = {2},
pages = {119-147},
optmonth = {},
era = {A},
abstract = {In this paper, we show how techniques from first-order
theorem proving can be used for efficient deductive
database updates. The key idea is to transform the given
database, together with the update request, into a
(disjunctive) logic program and to apply the hyper tableaux
calculus to solve the original update problem. The
resulting algorithm has the following properties: it works
goal-directed (i.e.\ the search is driven by the update
request), it is rational in the sense that it satisfies
certain rationality postulates stemming from philosophical
works on belief dynamics, and, unlike comparable
approaches, it is of polynomial space complexity. \\ To
obtain soundness and completeness results, the hyper
tableau calculus is slightly modified for minimal model
reasoning. Besides a direct proof we give an alternate
proof which gives insights into the relation to previous
approaches. As a by-product we thereby derive a soundness
and completeness result of hyper tableaux for computing
minimal abductive explanations.},
url = {ftp-final.pdf},
optannote = {}
}
@inproceedings{Baumgartner:FDPLL:CADE:00,
author = {Peter Baumgartner},
title = {{FDPLL -- A First-Order Davis-Putnam-Logeman-Loveland
Procedure}},
pages = {200--219},
crossref = {CADE:00},
era = {A},
url = {FDPLL-CADE-17.pdf},
doi = {10.1007/10721959_16},
abstract = {FDPLL is a directly lifted version of the well-known
Davis-Putnam-Logeman-Loveland (DPLL) procedure. While DPLL
is based on a splitting rule for case analysis wrt.\ ground
and complementary literals, FDPLL uses a lifted splitting
rule, i.e.\ the case analysis is made wrt.\ non-ground and
complementary literals now. \par The motivation for this
lifting is to bring together successful first-order
techniques like unification and subsumption to the
propositionally successful DPLL procedure. \par At the
heart of the method is a new technique to represent
first-order interpretations, where a literal specifies
truth values for all its ground instances, unless there is
a more specific literal specifying opposite truth values.
Based on this idea, the FDPLL calculus is developed and
proven as strongly complete.}
}
@inproceedings{Baumgartner:Massacci:TamingXOR:CL2000:00,
author = {Peter Baumgartner and Fabio Massacci},
title = {{The Taming of the (X)OR}},
abstract = {Many key verification problems such as bounded
model-checking, circuit verification and logical
cryptanalysis are formalized with combined clausal and
affine logic (i.e. clauses with xor as the connective) and
cannot be efficiently (if at all) solved by using CNF-only
provers. \par We present a decision procedure to
efficiently decide such problems. The Gauss-DPLL procedure
is a tight integration in a unifying framework of a
Gauss-Elimination procedure (for affine logic) and a
Davis-Putnam-Logeman-Loveland procedure (for usual clause
logic). \par The key idea, which distinguishes our approach
from others, is the full interaction bewteen the two parts
which makes it possible to maximise (deterministic)
simplification rules by passing around newly created unit
or binary clauses in either of these parts. We show the
correcteness and the termination of Gauss-DPLL under very
liberal assumptions.},
url = {http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-2-2000.ps.gz},
crossref = {CL2000:00},
optkey = {},
pages = {508--522},
optyear = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
optpublisher = {},
optannote = {}
}
@techreport{baumgartner:zhang:5:2000,
author = {Peter Baumgartner and Hantao Zhang~(Eds.)},
title = {{FTP 2000 -- Third International Workshop on First-Order
Theorem Proving, St Andrews, Scotland, July 2000}},
institution = {Universit{\"a}t Koblenz-Landau},
year = {2000},
type = {Fachberichte Informatik},
number = {5--2000},
language = {english},
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-5-2000/},
abstract = {FTP 2000 is the third in a series of workshops on
First-Order Theorem Proving. Following the successes of the
first workshop (FTP'97) in RISC Linz, Schloss Hagenberg,
Austria, and the second (FTP'98) in Vienna, Austria, this
year's workshop will be held in St Andrews, Scotland, in
conjunction with {\em Tableaux 2000\/}, the major
international conference for automated reasoning with
analytic tableaux and related methods ({\tt
http://i12www.ira.uka.de/TABLEAUX/}). Like the preceding
workshops in this series, FTP 2000 provides a forum for
presentation of recent work and discussion of research in
progress on First-order Theorem Proving as a core theme of
automated deduction. More information about the FTP
workshop series is available from the web page {\tt
http://www.logic.at/FTP/}. \par The technical program of
FTP 2000 consists of three invited talks, 18 regular
papers, and two position papers. The topics of these papers
match very well those of the workshop which cover automated
theorem proving in first-order classical, many-valued, and
modal logics, including nonexclusively: resolution,
equational reasoning, term-rewriting, model construction,
constraint reasoning, unification, propositional logic,
specialized decision procedures; strategies and complexity
of theorem proving procedures; and applications of
first-order theorem provers to problems in verification,
artificial intelligence, and mathematics.}
}
@proceedings{CADE:00,
booktitle = {CADE-17 -- The 17th International Conference on Automated
Deduction},
editor = {David McAllester},
year = {2000},
volume = {1831},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
title = {Automated Deduction -- CADE-17}
}
@proceedings{CL2000:00,
booktitle = {Computational Logic -- CL 2000},
editor = {John Lloyd and Veronica Dahl and Ulrich Furbach and
Manfred Kerber and Kung-Kiu Lau and Catuscia Palamidessi
and Luis Moniz Pereira and Yehoshua Sagiv and Peter J.
Stuckey},
year = {2000},
volume = {1861},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
title = {Computational Logic -- CL 2000}
}
@proceedings{Baumgartner:etal:ModelComputation:WS:CADE:00,
title = {CADE-17 Workshop on Model Computation - Principles,
Algorithms, Applications},
booktitle = {CADE-17 Workshop on Model Computation - Principles,
Algorithms, Applications},
year = {2000},
note = {http://www.uni-koblenz.de/{\textasciitilde}peter/CADE17-WS-MODELS/},
url = {http://www.uni-koblenz.de/~peter/CADE17-WS-MODELS/},
editor = {Peter Baumgartner and Chris Ferm{\"u}ller and Nicolas
Peltier and Hantao Zhang}
}