peter-2000.bib

@comment{{This file has been generated by bib2bib 1.95}}
@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}
}