SEKI-Reports of the research groups Avenhaus and Madlener

Quick reference: 1998, 1997, 1996, 1995, 1994, 1993, 1992, 1991.

• Fuchs, D.:
  Cooperation between Top-Down and Bottom-Up Theorem Provers by Subgoal Clause Transfer,
  SEKI-Report SR-98-01, University of Kaiserslautern, 1998.
  • Abstract
  • Download full paper (77 Kbytes)
• Fuchs, D.:
  Requirement-Based Cooperative Theorem Proving,
  SEKI-Report SR-98-02, University of Kaiserslautern, 1998.
  • Abstract
  • Download full paper (90Kbytes)

• Fuchs, M.:
  Flexible Re-enactment of Proofs,
  SEKI-Report SR-97-01, University of Kaiserslautern, 1997.
  • Abstract
  • Download full paper (71 Kbytes)
• Eschbach, R. ; Sonntag, I.:
  PLATIN: A Planning System for Inductive Theorem Proving - Implementation and Experiences,
  SEKI-Report SR-97-02, University of Kaiserslautern, 1997.
  • Abstract
  • Download full paper (140 Kbytes)
• Denzinger, J. ; Fuchs, D.:
  Cooperation in Theorem Proving by Loosely Coupled Heuristics,
  SEKI-Report SR-97-03, University of Kaiserslautern, 1997.
  • Abstract
  • Download full paper (101 Kbytes)
• Denzinger, J. ; Scholz, S.:
  Using Teamwork for the Distribution of Approximately Solving the Traveling Salesman Problem with Genetic Algorithms,
  SEKI-Report SR-97-04, University of Kaiserslautern, 1997.
  • Abstract
  • Download full paper (109 Kbytes)
• Fuchs, D.:
  Coupling Saturation-Based Provers by Exchanging Positive/Negative Information,
  SEKI-Report SR-97-07, University of Kaiserslautern, 1997.
  • Abstract
  • Download full paper (113 Kbytes)
• Denzinger, J. ; Fuchs, D.:
  Knowledge-based Cooperation between Theorem Provers by TECHS,
  SEKI-Report SR-97-11, University of Kaiserslautern, 1997.
  • Abstract
  • Download full paper (80 Kbytes)

• Buch, A. ; Hillenbrand, T.:
  WALDMEISTER: Development of a High Performance Completion-Based Theorem Prover,
  SEKI-Report SR-96-01, University of Kaiserslautern, 1996.
  • Abstract
  • Download full paper (240 Kbytes)
• Becker, K.:
  How to Prove Ground Confluence,
  SEKI-Report SR-96-02, University of Kaiserslautern, 1996.
  • Abstract
  • Download full paper (88 Kbytes)
• Fuchs, M.:
  Towards Full Automation of Deduction: A Case Study,
  SEKI-Report SR-96-07, University of Kaiserslautern, 1996.
  • Abstract
  • Download full paper (91 Kbytes)
• Fuchs, M.:
  Evolving Combinators,
  SEKI-Report SR-96-08, University of Kaiserslautern, 1996.
  • Abstract
  • Download full paper (68 Kbytes)
• Denzinger, J. ; Fuchs, M. ; Fuchs, M.:
  High Performance ATP Systems by Combining Several AI Methods,
  SEKI-Report SR-96-09, University of Kaiserslautern, 1996.
  • Abstract
  • Download full paper (97 Kbytes)
• Kuehler, U. ; Wirth, C.-P.:
  Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving,
  SEKI-Report SR-96-11, University of Kaiserslautern, 1996.
  • Abstract
  • Download full paper (100 Kbytes)
• Fuchs, D.:
  Inference Rights for Controlling Search in Generating Theorem Provers,
  SEKI-Report SR-96-12, University of Kaiserslautern, 1996.
  • Abstract
  • Download full paper (78 Kbytes)

• Reinert, B. ; Madlener, K.:
  On Groebner Bases for Two-Sided Ideals in Nilpotent Group Rings,
  SEKI-Report SR-95-01, University of Kaiserslautern, 1995.
  • Abstract
  • Download full paper (110 Kbytes)
• Fuchs, M.:
  Learning proof heuristics by adapting parameters,
  SEKI-Report SR-95-02, University of Kaiserslautern, 1995.
  • Abstract
  • Download full paper (151 Kbytes)
• Avenhaus, J. ; Loria-Saenz, C. ; Steinbach, J.:
  A Reduction Ordering for Higher-Order Terms,
  SEKI-Report SR-95-03, University of Kaiserslautern, 1995.
  • Abstract
  • Download full paper (71 Kbytes)
• Plaisted, D.A. ; Sattler-Klein, A.:
  Proof Lengths for Equational Completion,
  SEKI-Report SR-95-06, University of Kaiserslautern, 1995.
  • Abstract
  • Download full paper (100 Kbytes)
• Avenhaus, J. ; Plaisted, D.A.:
  General Algorithms for Permutations in Equational Inference,
  SEKI-Report SR-95-07, University of Kaiserslautern, 1995.
  • Abstract
  • Download full paper (132 Kbytes)
• Gramlich, B.:
  A Note on a Paramterized Version of the Well-Founded Induction Principle,
  SEKI-Report SR-95-08, University of Kaiserslautern, 1995.
  • Abstract
  • Download full paper (49 Kbytes)
• Wirth, C.-P.:
  Syntactic Confluence Criteria for Positive/Negative-Conditional Term Rewriting Systems,
  SEKI-Report SR-95-09, University of Kaiserslautern, 1995.
  • Abstract
  • Download full paper (532 Kbytes)
• Fuchs, M.:
  Experiments in the Heuristic Use of Past Proof Experience,
  SEKI-Report SR-95-10, University of Kaiserslautern, 1995.
  • Abstract
  • Download full paper (164 Kbytes)
• Denzinger, J.:
  Completion and Equational Theorem Proving using Taxonomic Constraints,
  SEKI-Report SR-95-11, University of Kaiserslautern, 1995.
  • Abstract
  • Download full paper (71 Kbytes)
• Gramlich, B.:
  Confluence without Termination via Parallel Critical Pairs,
  SEKI-Report SR-95-13, University of Kaiserslautern, 1995.
  • Abstract
  • Download full paper (85 Kbytes)
• Avenhaus, J. ; Maldener, K.:
  Theorem Proving in Hierarchical Clausal Specifications,
  SEKI-Report SR-95-14, University of Kaiserslautern, 1995.
  • Abstract
  • Download full paper (160 Kbytes)
• Wirth, C.-P. ; Kühler, U.:
  Inductive Theorem Proving in Theories Specified by Positive/Negative-Conditional Equations,
  SEKI-Report SR-95-15, University of Kaiserslautern, 1995.
  • Abstract
  • Download full paper (300 Kbytes)

• Fuchs, M.:
  The application of goal-oriented heuristics for proving equational theorems via the unfailing Knuth-Bendix completion procedure. A case study: lattice ordered groups,
  SEKI-Report SR-94-02, University of Kaiserslautern, 1994.
  • Abstract
  • Download full paper (81 Kbytes)
• Fuchs, M.:
  An alternative for handling AC,
  SEKI-Report SR-94-03, University of Kaiserslautern, 1994.
  • Abstract
  • Download full paper (53 Kbytes)
• Denzinger, J. ; Fuchs, M.:
  Goal oriented equational theorem proving using team work,
  SEKI-Report SR-94-04, University of Kaiserslautern, 1994.
  • Abstract
  • Download full paper (85 Kbytes)
• Denzinger, J. ; Schulz, S.:
  Analysis and Representation of Equational Proofs Generated by a Distributed Completion Based Proof System,
  SEKI-Report SR-94-05, University of Kaiserslautern, 1994.
  • Abstract
  • Download full paper (253 Kbytes)
• Denzinger, J. ; Kronenburg, M.:
  Planning for distributed theorem proving: The team work approach,
  SEKI-Report SR-94-09, University of Kaiserslautern, 1994.
  • Abstract
  • Download full paper (78 Kbytes)

• Fuchs, M.:
  Using theorem provers for PL1EQ as inductive provers,
  SEKI-Report SR-93-01, University of Kaiserslautern, 1993.
  • Abstract
  • Download full paper (86 Kbytes)
• Sonntag, I. ; Denzinger, J.:
  Extending automatic theorem proving by planning,
  SEKI-Report SR-93-02, University of Kaiserslautern, 1993.
  • Abstract
  • Download full paper (107 Kbytes)
• Avenhaus, J. ; Loria-Saenz, C.:
  Canonical Conditional Rewrite Systems Containing Extra Variables,
  SEKI-Report SR-93-03, University of Kaiserslautern, 1993.
  • Abstract
  • Download full paper (103 Kbytes)
• Avenhaus, J. ; Denzinger, J.:
  Distributing equational theorem proving,
  SEKI-Report SR-93-06, University of Kaiserslautern, 1993.
  • Abstract
  • Download full paper (88 Kbytes)
• Madlener, K. ; Reinert, B.:
  On Groebner Bases in Monoid and Group Rings,
  SEKI-Report SR-93-08, University of Kaiserslautern, 1993.
  • Abstract
  • Download full paper (222 Kbytes)
• Gramlich, B.:
  Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems,
  SEKI-Report SR-93-09, University of Kaiserslautern, 1993.
  • Abstract
  • Download full paper (156 Kbytes)
• Avenhaus, J. ; Denzinger, J. (eds.):
  Informal proceesings of the Annual Meeting of "GI-Fachgruppe 'Deduktionssysteme'" in Kaiserslautern, 1993,
  SEKI-Report SR-93-11, University of Kaiserslautern, 1993.
  • Abstract
  • Download full paper (88 Kbytes)
• Gramlich, B.:
  New Abstract Criteria for Termination and Confluence of Conditional Rewrite Systems,
  SEKI-Report SR-93-17, University of Kaiserslautern, 1993.
  • Abstract
  • Download full paper (143 Kbytes)
• Steinbach, J.:
  On the Complexity of Simplification Orderings,
  SEKI-Report SR-93-18, University of Kaiserslautern, 1993.
  • Abstract
  • Download full paper (90 Kbytes)
• Sattler-Klein, A.:
  About Changing the Ordering during Knuth-Bendix Completion,
  SEKI-Report SR-93-19, University of Kaiserslautern, 1993.
  • Abstract
  • Download full paper (109 Kbytes)

• Deiß T.:
  Conditional semi-Thue Systems for Presenting Monoids,
  SEKI-Report SR-92-12, University of Kaiserslautern, 1992.
  • Abstract
  • Download full paper (143 Kbytes)
• Steinbach, J.:
  Notes on Transformation Orderings,
  SEKI-Report SR-92-23, University of Kaiserslautern, 1992.
  • Abstract
  • Download full paper (163 Kbytes)

• Steinbach, J.:
  Termination Proofs of Rewriting Systems - Heuristics for Generating Polynomial Orderings,
  SEKI-Report SR-91-14, University of Kaiserslautern, 1991.
  • Abstract
  • Download full paper (168 Kbytes)
• Gramlich, B. ; Lindner, W.:
  A Guide to UNICOM, an Inductive Theorem Prover Based on Rewriting and Completion Techniques,
  SEKI-Report SR-91-17, University of Kaiserslautern, 1991.
  • Abstract
  • Download full paper (128 Kbytes)

Last Change: 11/02/2000