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

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