peter-1994.bib

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

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

@article{Baumgartner:Furbach:RME:JAR:94,
  author = {Peter Baumgartner and Ulrich Furbach},
  title = {{Model Elimination without Contrapositives and its
		  Application to PTTP}},
  journal = {Journal of Automated Reasoning},
  year = {1994},
  era = {A},
  volume = {13},
  pages = {339--359},
  url = {nocontra-jar.pdf},
  abstract = { We give modifications of model elimination which do not
		  necessitate the use of contrapositives. These restart model
		  elimination calculi are proven sound and complete and their
		  implementation by PTTP is depicted. The corresponding proof
		  procedures are evaluated by a number of runtime experiments
		  and they are compared to other well known provers. Finally
		  we relate our results to other calculi, namely the
		  connection method, modified problem reduction format and
		  Near-Horn Prolog. },
  optnote = {Short version in: Proceedings of CADE-12, Springer LNAI
		  814, 1994, pp 87--101}
}

@inproceedings{Baumgartner:TME:ECAI:94,
  author = {Peter Baumgartner},
  title = {{Refinements of Theory Model Elimination and a Variant
		  without Contrapositives}},
  booktitle = {11th European Conference on Artificial Intelligence, ECAI
		  94},
  year = {1994},
  editor = {A.G. Cohn},
  publisher = {Wiley},
  era = {A},
  url = {ecai-final.pdf},
  abstract = {Theory Reasoning means to build-in certain knowledge about
		  a problem domain into a deduction system or calculus, such
		  as model elimination. We present several complete versions
		  of highly restricted theory model elimination (TME)
		  calculi. These restrictions allow (1) to keep fewer path
		  literals in extension steps than in related calculi, and
		  (2) to discard proof attempts with multiple occurrences of
		  literals along a path (i.e.\ regularity holds). On the
		  other hand, we obtain by small modifications to TME
		  versions which do not need contrapositives ({\`a} la
		  Near-Horn Prolog). We show how regularity can be adapted
		  for these versions. The {\em independence of the goal
		  computation rule\/} holds for all variants. Comparative
		  runtime results for our PTTP-implementations are supplied.},
  optpages = {90--94},
  optannote = { }
}

@inproceedings{Baumgartner:Furbach:RME:CADE12:94,
  author = {Peter Baumgartner and Ulrich Furbach},
  title = {{Model Elimination without Contrapositives}},
  booktitle = {Automated Deduction -- CADE-12},
  year = {1994},
  editor = {A. Bundy},
  publisher = {Springer},
  pages = {87--101},
  volume = {814},
  era = {A},
  series = {Lecture Notes in Artificial Intelligence},
  url = {nocontra-cade-final.pdf},
  abstract = { We present modifications of model elimination which do
		  not necessitate the use of contrapositives. These restart
		  model elimination calculi are proven sound and complete.
		  The corresponding proof procedures are evaluated by a
		  number of runtime experiments and they are compared to
		  other well known provers. Finally we relate our results to
		  other calculi, namely the connection method, modified
		  problem reduction format and Near-Horn Prolog. }
}

@inproceedings{Baumgartner:Furbach:PROTEIN:CADE12:94,
  author = {Peter Baumgartner and Ulrich Furbach},
  title = {{PROTEIN: A {\em PRO\/}ver with a {\em T\/}heory {\em
		  E\/}xtension {\em I\/}nterface}},
  booktitle = {Automated Deduction -- CADE-12},
  year = {1994},
  editor = {A. Bundy},
  publisher = {Springer},
  pages = {769--773},
  volume = {814},
  era = {A},
  series = {Lecture Notes in Artificial Intelligence},
  url = {protein-cade-final.pdf},
  abstract = {PROTEIN ({\em PRO\/}ver with a {\em T\/}heory {\em
		  E\/}xtension {\em IN\/}terface) is a PTTP-based first order
		  theorem prover over built-in theories. Besides various
		  standard-refinements known for model elimination, PROTEIN
		  also offers a variant of model elimination for case-based
		  reasoning and which does not need contrapositives. },
  optnote = {Available in the WWW, URL: {\small\tt
		  http://www.uni-koblenz.de/ag-ki/Systems/PROTEIN/}}
}

@inproceedings{Baumgartner:94b,
  author = {Peter Baumgartner and J{\"u}rgen Dix and Ulrich Furbach
		  and Frieder Stolzenburg},
  title = {{The Spectrum of Model Elimination based Theorem
		  Proving}},
  booktitle = {Informal Proceedings of the 11th Annual Meeting of the
		  GI-Fachgruppe Deduktionssysteme},
  organization = {TH Darmstadt},
  year = {1994},
  editor = {W. Bibel, C. Walther},
  number = {AIDA-94-06},
  series = {Research Report},
  optannote = { }
}

@inproceedings{Baumgartner:94c,
  author = {Peter Baumgartner},
  title = {{A Transformation Technique to Combine the Linear and the
		  Unit-Resulting Restrictions}},
  booktitle = {Proceedings of the Eight International Symposium on
		  Methodologies for Intelligent Systems},
  organization = {Oak Ridge National Laboratory},
  year = {1994},
  address = {Charlotte, N.C, USA},
  optannote = { }
}

@inproceedings{Baumgartner:Furbach:94c,
  author = {Peter Baumgartner and Ulrich Furbach},
  title = {{Model Elimination without Contrapositives and its
		  Application to PTTP}},
  booktitle = {TABLEAUX-'94 Workshop},
  organization = {Imperial College},
  year = {1994},
  editor = {Broda D'Agostino Gor{\'e} Johnson Reeves},
  number = {TR-94/5},
  series = {Technical Report},
  optannote = { }
}

@inproceedings{Baumgartner:Furbach:94d,
  author = {Peter Baumgartner and Ulrich Furbach},
  title = {{Lineare Vervollst{\"a}ndigung f{\"u}r die Behandlung von
		  Horntheorien}},
  booktitle = {DFG-Colloquium ``Deduction''},
  organization = {Technische Hochschule Darmstadt},
  year = {1994},
  number = {AIDA-94-02},
  series = {Research Report},
  optannote = { }
}

@misc{Baumgartner:Furbach:94e,
  author = {Peter Baumgartner and Ulrich Furbach},
  title = {{The Spectrum of Model Elimination Based Theorem
		  Proving}},
  year = {1994},
  howpublished = {Proc. of the Workshop ``Automated Reasoning: Bridging the
		  Gap between Theory and Practice''},
  note = {Leeds, England},
  optannote = { }
}

@inproceedings{Baumgartner:Furbach:Stolzenburg:94,
  author = {Peter Baumgartner and Ulrich Furbach and Frieder
		  Stolzenburg},
  title = {{Applications of Theory Reasoning in Model Elimination}},
  booktitle = {Theory Reasoning in Automated Deduction},
  year = {1994},
  editor = {Peter Baumgartner and H.-J. B{\"u}rckert and H. Comon and
		  Ulrich Furbach and Mark Stickel},
  series = {CADE-12 Workshop Proceedings},
  optannote = { }
}

@proceedings{Baumgartner:etal:94,
  title = {{Theory Reasoning in Automated Deduction}},
  organization = {INRIA, Lorraine},
  year = {1994},
  editor = {Peter Baumgartner, H.-J. B{\"u}rckert and H. Comon},
  note = {Technical Report},
  series = {12th International Conference on Automated Deduction,
		  Workshop},
  optannote = { }
}

@inproceedings{Stolzenburg:Baumgartner:94b,
  author = {Frieder Stolzenburg and Peter Baumgartner},
  title = {{Constraint Model Elimination and a PTTP-Implementation}},
  booktitle = {Workshop on Constraint Languages and their Use in Problem
		  Modelling --- International Logic Programming Symposium},
  year = {1994},
  editor = {J. Jourdan, P. Lim, R. Yap},
  optannote = { }
}