peter-1992.bib

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

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

@inproceedings{Baumgartner:OrderedTheoryResolution:LPAR:92,
  author = {Peter Baumgartner},
  title = {{An Ordered Theory Resolution Calculus}},
  booktitle = {Logic Programming and Automated Reasoning (Proceedings)},
  year = {1992},
  month = {July},
  editor = {A. Voronkov},
  publisher = {Springer},
  address = {St. Petersburg, Russia},
  era = {A},
  pages = {119--130},
  series = {Lecture Notes in Artificial Intelligence},
  volume = {624},
  url = {lparfinal.pdf},
  abstract = {In this paper we present an ordered theory resolution
		  calculus and prove its completeness. Theory reasoning means
		  to relieve a calculus from explicitly drawing inferences in
		  a given theory by special purpose inference rules (e.g.
		  E-resolution for equality reasoning). We take advantage of
		  orderings (e.g. simplification orderings) by disallowing to
		  resolve upon clauses which violate certain maximality
		  constraints; stated positively, a resolvent may only be
		  built if all the selected literals are maximal in their
		  clauses. By this technique the search space is drastically
		  pruned. As an instantiation for theory reasoning we show
		  that equality can be built in by rigid E-unification. }
}

@inproceedings{Baumgartner:TME:GWAI:92,
  author = {Peter Baumgartner},
  title = {{A Model Elimination Calculus with Built-in Theories}},
  booktitle = {GWAI-92 --- Proceedings of the 16\/$^{th}$ German Workshop
		  on Artificial Intelligence},
  url = {gwai-final.pdf},
  year = {1992},
  editor = {H.-J. Ohlbach},
  publisher = {Springer},
  pages = {30--42},
  series = {Lecture Notes in Artificial Intelligence},
  volume = {671},
  abstract = {The {\em model elimination calculus} is a linear,
		  refutationally complete calculus for first order clause
		  logic. We show how to extend this calculus with a framework
		  for {\em theory reasoning}. Theory reasoning means to
		  separate the knowledge of a given domain or theory and
		  treat it by special purpose inference rules. We present two
		  versions of theory model elimination: the one is called
		  {\em total theory model elimination} (which allows e.g. to
		  treat equality in a rigid E-resolution style), and the
		  other is called {\em partial theory model elimination}
		  (which allows e.g. to treat equality in a paramodulation
		  style). }
}

@inproceedings{Baumgartner:92d,
  author = {Peter Baumgartner},
  title = {{A Model Elimination Calculus with Built-In Theories}},
  booktitle = {Theorem Proving with Analytic Tableaux and Related
		  Methods},
  year = {1992},
  editor = {{Fronh{\"o}fer, H{\"a}hnle, K{\"a}ufl}},
  number = {8/92},
  series = {Technical Report},
  optannote = { }
}

@inproceedings{Baumgartner:92b,
  author = {Peter Baumgartner},
  title = {{Partial Unification for Ordered Theory Resolution}},
  booktitle = {6th International Workshop on Unification},
  organization = {IBFI Dagstuhl},
  year = {1992},
  editor = {F. Baader and J. Siekmann and W. Snyder},
  note = {Dagstuhl Seminar Report 42}
}

@inproceedings{Baumgartner:Furbach:92a,
  author = {Peter Baumgartner},
  title = {{Consolution as a Framework for Comparing Calculi}},
  booktitle = {Theorem Proving with Analytic Tableaux and Related
		  Methods},
  year = {1992},
  editor = {{Fronh{\"o}fer, H{\"a}hnle, K{\"a}ufl}},
  number = {8/92},
  series = {Technical Report},
  optannote = { }
}

@techreport{Baumgartner:Furbach:Petermann:UnifiedApproachTheoryReasoning:TechRep:15:92,
  author = {Peter Baumgartner and Ulrich Furbach and Uwe Petermann},
  title = {{A Unified Approach to Theory Reasoning}},
  institution = {Universit{\"a}t Koblenz-Landau},
  type = {Fachberichte Informatik},
  address = {Institut f{\"u}r Informatik, Rheinau 1, D-56075
		  Koblenz},
  year = {1992},
  url = {thover.pdf},
  abstract = {{\em Theory reasoning} is a kind of two-level reasoning in
		  automated theorem proving, where the knowledge of a given
		  domain or theory is separated and treated by special
		  purpose inference rules. We define a classification for the
		  various approaches for theory reasoning which is based on
		  the syntactic concepts of {\em literal level --- term level
		  --- variable level\/}. The main part is a review of theory
		  extensions of common calculi (resolution, model elimination
		  and a connection method). In order to see the relationships
		  among these calculi, we define a super-calculus called {\em
		  theory consolution\/}. Completeness of the various theory
		  calculi is proven. Finally, due to its relevance in
		  automated reasoning, we describe current ways of equality
		  handling.},
  number = {15/92}
}