peter-1995.bib

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

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

@inproceedings{Baumgartner:Stolzenburg:CME:Tableaux:95,
  author = {Peter Baumgartner and Frieder Stolzenburg},
  title = {{Constraint Model Elimination and a PTTP-Implementation}},
  pages = {201--216},
  url = {rheinfels.pdf},
  era = {A},
  abstract = {In constraint logic programming, proof procedures for {\em
		  Horn} clauses are enhanced with an interface to efficient
		  constraint solvers. In this paper we show how to
		  incorporate constraint processing into a general, non-Horn
		  theorem proving calculus. \par A framework for a new
		  calculus is introduced which combines model elimination
		  with constraint solving, following the lines of
		  B{\"u}rckert (1991). A prototype system has been
		  implemented rapidly by only combining a PROLOG technology
		  implementation of model elimination and PROLOG with
		  constraints. Some example studies, e.g. taxonomic
		  reasoning, show the advantages and some problems with this
		  procedure.},
  crossref = {TABLEAUX:95}
}

@misc{Baumgartner:Furbach:Stolzenburg:95b,
  author = {Peter Baumgartner and Ulrich Furbach and Frieder
		  Stolzenburg},
  title = {{Computing Answers and Logic Programming by Model
		  Elimination Based Theorem Proving}},
  year = {1995},
  howpublished = {Proc. of the Workshop ``Automated Reasoning: Bridging the
		  Gap between Theory and Practice''},
  note = {Leeds, England},
  optannote = { }
}

@techreport{Baumgartner:Schumann:RMESETHEO:TechRep:5:95,
  author = {Peter Baumgartner and Johann Schumann},
  title = {{Implementing Restart Model Elimination and Theory Model
		  Elimination on top of SETHEO}},
  institution = {Universit{\"a}t Koblenz-Landau},
  type = {Fachberichte Informatik},
  address = {Institut f{\"u}r Informatik, Rheinau 1, D-56075
		  Koblenz},
  url = {http://www.uni-koblenz.de/fb4/publikationen/ gelbereihe/RR-5-95.ps.gz},
  year = {1995},
  number = {5--95},
  abstract = {This paper presents an implementation for the efficient
		  execution of Theory Model Elimination (TME), TME by
		  Linearizing Completion, and Restart Model Elimination (RME)
		  on top of the automated theorem prover {\small SETHEO}.
		  These calculi allow for theory reasoning using a Model
		  Elimination based theorem prover. They are described in
		  detail and their major properties are shown. Then, a
		  detailed description how TME by Linearizing Completion and
		  RME can be implemented on top of {\small SETHEO}'s Abstract
		  Machine (SAM) is given. Due to the flexibility of the
		  Abstract Machine and its input language LOP, only simple
		  transformations of the input formula are sufficient to
		  obtain an efficient implementation. Only for RME, one
		  machine-instruction of the SAM had to be modified slightly.
		  We present results of experiments comparing plain {\small
		  SETHEO} with an implementation of TME with PTTP (PROTEIN)
		  and the {\small SETHEO} implementation presented here.}
}

@article{Baumgartner:Stolzenburg:DeduktionstreffenBericht:95,
  author = {Peter Baumgartner and Frieder Stolzenburg},
  title = {{Jahrestreffen der GI-Fachgruppe 1.2.1 Deduktion}},
  journal = {KI},
  year = 1995,
  volume = 9,
  number = 6,
  pages = {80-81},
  note = {Conference report}
}

@proceedings{TABLEAUX:95,
  booktitle = {Theorem Proving with Analytic Tableaux and Related
		  Methods},
  title = {Theorem Proving with Analytic Tableaux and Related
		  Methods},
  year = {1995},
  editor = {Peter Baumgartner and Reiner H{\"a}hnle and J. Posegga},
  publisher = {Springer},
  volume = {918},
  series = {Lecture Notes in Artificial Intelligence}
}