@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} }