peter-1999.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bib2bib -c 'year=1999 and not annote:"skip_html" and not annote:"unpublished"' -ob peter-1999.bib -oc peter-1999.cite peter.bib}}

@inproceedings{Baumgartner:Kuehn:AbductiveCoreference:ICOS:99,
  author = {Peter Baumgartner and Michael K{\"u}hn},
  title = {Abductive Coreference by Model Construction},
  booktitle = {ICoS-1 Inference in Computational Semantics},
  optcrossref = {},
  optkey = {},
  optpages = {},
  year = {1999},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  address = {Institute for Logic, Language and Computation, University
		  of Amsterdam},
  month = {August},
  optorganization = {},
  optpublisher = {},
  optnote = {},
  url = {http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-6-99.ps.gz},
  abstract = {In this paper, we argue that the resolution of anaphoric
		  expressions in an utterance is essentially an {\em
		  abductive\/} task following [HSAM93] 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 {\em hyper tableaux\/} [BFN96,
		  K{\"u}h97] 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 abuctive explanations. This abductive
		  inference is applied to the resolution of anaphoric
		  expressions in our general model constructing framework for
		  incremental discourse representation [K{\"u}h99] which we
		  argue to be useful for computing information updates from
		  natural language utterances [Vel96].}
}

@inproceedings{Baumgartner:Eisinger:Furbach:CCC:CADE:99,
  author = {Peter Baumgartner and Norbert Eisinger and Ulrich
		  Furbach},
  title = {A Confluent Connection Calculus},
  crossref = {CADE:99},
  era = {A},
  pages = {329--343},
  url = {http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-23-98.ps.gz},
  abstract = {This work is concerned with basic issues of the design of
		  calculi and proof procedures for first-order connection
		  methods and tableaux calculi. Proof procedures for these
		  type of calculi developed so far suffer from not exploiting
		  proof confluence, and very often unnecessarily rely on a
		  heavily backtrack oriented control regime. \par As a new
		  result, we present a variant of a connection calculus and
		  prove its {\em strong\/} completeness. This enables the
		  design of backtrack-free control regimes. To demonstrate
		  that the underlying fairness condition is reasonably
		  implementable we define an effective search strategy.}
}

@inproceedings{Baumgartner:Horton:Spencer:MergePathHyperTableaux:Tableaux:99,
  author = {Peter Baumgartner and J.D. Horton and Bruce Spencer},
  title = {Merge Path Improvements for Minimal Model Hyper Tableaux},
  optbooktitle = {},
  crossref = {TABLEAUX:99},
  optkey = {},
  optpages = {},
  optyear = {},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  era = {A},
  optmonth = {},
  optorganization = {},
  optpublisher = {},
  optnote = {},
  optannote = {},
  abstract = {We combine techniques originally developed for
		  refutational first-order theorem proving within the clause
		  tree framework with techniques for minimal model
		  computation developed within the hyper tableau framework.
		  This combination generalizes well-known tableaux techniques
		  like complement splitting and folding-up/down. We argue
		  that this combination allows for efficiency improvements
		  over previous, related methods. It is motivated by
		  application to diagnosis tasks; in particular the problem
		  of avoiding redundancies in the diagnoses of electrical
		  circuits with reconvergent fanouts is addressed by the new
		  technique. In the paper we develop as our main contribution
		  in a more general way a sound and complete calculus for
		  propositional circumscriptive reasoning in the presence of
		  minimized and varying predicates. },
  url = {http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-1-99.ps.gz}
}

@inproceedings{Baumgartner:Schaefer:CouplingKIVPROTEIN:TOOLS98:99,
  author = {Peter Baumgartner and Dorothea Sch{\"a}fer},
  title = {Model Elimination with Simplification and its Application
		  to Software Verification},
  booktitle = {Tool Support for System Specification, Development, and
		  Verification},
  optcrossref = {},
  optkey = {},
  optpages = {},
  publisher = {Springer-Verlag Wien NewYork},
  year = {1999},
  editor = {Rudolf Berghammer and Yassine Lakhnech},
  series = {Advances in Computer Science},
  optnumber = {},
  opttype = {},
  optchapter = {},
  optaddress = {},
  optedition = {},
  optmonth = {},
  optannote = {},
  abstract = {This paper describes our approach of coupling the
		  interactive software verification system KIV with the Model
		  Elimination based, complete automated theorem prover
		  PROTEIN. In order to make this combination work in
		  practice, we propose to incorporate domain knowledge
		  readily given from the KIV domain into PROTEIN. More
		  specifically, we extend Model Elimination by a concept of
		  simplification based on conditional rewrite rules. The
		  extension is defined in such a way that rewrite rules as
		  given from the KIV system can easily be accommodated. This
		  yields better performance for proof automatization and thus
		  relieves the system engineer from more interactions. In the
		  paper, we describe the new simplification technique, show
		  completeness, and demonstrate the benefits with practical
		  experiments from the KIV domain.},
  url = {tools98-final-conform.pdf}
}

@incollection{Baumgartner:Eisinger:Furbach:CCC:WB60:99,
  author = {Peter Baumgartner and Norbert Eisinger and Ulrich
		  Furbach},
  title = {A Confluent Connection Calculus},
  booktitle = {Intellectics and Computational Logic -- Papers in Honor of
		  Wolfgang Bibel},
  optpages = {},
  publisher = {Kluwer},
  year = {1999},
  editor = {Steffen H{\"o}lldobler},
  url = {http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-23-98.ps.gz},
  optchapter = {},
  optaddress = {},
  optmonth = {},
  optnote = {},
  optannote = {},
  abstract = {This work is concerned with basic issues of the design of
		  calculi and proof procedures for first-order connection
		  methods and tableaux calculi. Proof procedures for these
		  type of calculi developed so far suffer from not exploiting
		  proof confluence, and very often unnecessarily rely on a
		  heavily backtrack oriented control regime. \par As a new
		  result, we present a variant of a connection calculus and
		  prove its {\em strong\/} completeness. This enables the
		  design of backtrack-free control regimes. To demonstrate
		  that the underlying fairness condition is reasonably
		  implementable we define an effective search strategy. We
		  show that with the new approach the search space can be
		  exponentially smaller than those of current,
		  backtracking-oriented proof procedures based on {\em
		  weak\/} completeness results.}
}

@proceedings{TABLEAUX:99,
  booktitle = {Automated Reasoning with Analytic Tableaux and Related
		  Methods},
  title = {Automated Reasoning with Analytic Tableaux and Related
		  Methods},
  year = {1999},
  editor = {Neil Murray},
  publisher = {Springer},
  volume = {1617},
  series = {Lecture Notes in Artificial Intelligence}
}

@proceedings{CADE:99,
  booktitle = {CADE-16 -- The 16th International Conference on Automated
		  Deduction},
  editor = {Harald Ganzinger},
  year = {1999},
  volume = {1632},
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  title = {Automated Deduction -- CADE-16},
  address = {Trento, Italy}
}