@string{fbi     = "{FB Informatik, Universit\"at Kaiserslautern}"}

@string{spring  = "Springer"}

@string{lnai    = "LNAI"}
@string{lncs    = "LNCS"}

@string{jar     = "Journal of Automated Reasoning"}
@string{jsc     = "Journal of Symbolic Computation"}
@string{tcs     = "Theoretical Computer Science"}
@string{jai     = "Artificial Intelligence"}

@string{cade1   = "Proc. of the $1^{st}$ International Conference on Automated Deduction"}
@string{cade2   = "Proc. of the $2^{nd}$ International Conference on Automated Deduction"}
@string{cade3   = "Proc. of the $3^{rd}$ International Conference on Automated Deduction"}
@string{cade4   = "Proc. of the $4^{th}$ International Conference on Automated Deduction"}
@string{cade5   = "Proc. of the $5^{th}$ International Conference on Automated Deduction"}
@string{cade6   = "Proc. of the $6^{th}$ International Conference on Automated Deduction"}
@string{cade7   = "Proc. of the $7^{th}$ International Conference on Automated Deduction"}
@string{cade8   = "Proc. of the $8^{th}$ International Conference on Automated Deduction"}
@string{cade9   = "Proc. of the $9^{th}$ International Conference on Automated Deduction"}
@string{cade10  = "Proc. of the $10^{th}$ International Conference on Automated Deduction"}
@string{cade11  = "Proc. of the $11^{th}$ International Conference on Automated Deduction"}
@string{cade12  = "Proc. of the $12^{th}$ International Conference on Automated Deduction"}
@string{cade13  = "Proc. of the $13^{th}$ International Conference on Automated Deduction"}

@string{ctrs1 = "$1^{st}$ CTRS"}
@string{ctrs2 = "Proc. of the $2^{nd}$ International Workshop on Conditional and Typed Rewriting Systems"}
@string{ctrs3 = "Proc. of the $3^{rd}$ International Workshop on Conditional and Typed Rewriting Systems"}
@string{ctrs4 = "Proc. of the $4^{th}$ International Workshop on Conditional and Typed Rewriting Systems"}

@string{ijcai1  = "Proc. of the $1^{st}$ International Joint Conference on Artificial Intelligence"}
@string{ijcai2  = "Proc. of the $2^{nd}$ International Joint Conference on Artificial Intelligence"}
@string{ijcai3  = "Proc. of the $3^{rd}$ International Joint Conference on Artificial Intelligence"}
@string{ijcai4  = "Proc. of the $4^{th}$ International Joint Conference on Artificial Intelligence"}
@string{ijcai5  = "Proc. of the $5^{th}$ International Joint Conference on Artificial Intelligence"}
@string{ijcai6  = "Proc. of the $6^{th}$ International Joint Conference on Artificial Intelligence"}
@string{ijcai7  = "Proc. of the $7^{th}$ International Joint Conference on Artificial Intelligence"}
@string{ijcai8  = "Proc. of the $8^{th}$ International Joint Conference on Artificial Intelligence"}
@string{ijcai9  = "Proc. of the $9^{th}$ International Joint Conference on Artificial Intelligence"}
@string{ijcai10 = "Proc. of the $10^{th}$ International Joint Conference on Artificial Intelligence"}
@string{ijcai11 = "Proc. of the $11^{th}$ International Joint Conference on Artificial Intelligence"}
@string{ijcai12 = "Proc. of the $12^{th}$ International Joint Conference on Artificial Intelligence"}
@string{ijcai13 = "Proc. of the $13^{th}$ International Joint Conference on Artificial Intelligence"}


@string{lics3 = "$3^{rd}$ LICS"}

@string{rta1 = "Proc. of the $1^{st}$ International Conference on Rewriting Techniques and Applications"}
@string{rta2 = "Proc. of the $2^{nd}$ International Conference on Rewriting Techniques and Applications"}
@string{rta3 = "Proc. of the $3^{rd}$ International Conference on Rewriting Techniques and Applications"}
@string{rta4 = "Proc. of the $4^{th}$ International Conference on Rewriting Techniques and Applications"}
@string{rta5 = "Proc. of the $5^{th}$ International Conference on Rewriting Techniques and Applications"}
@string{rta6 = "Proc. of the $6^{th}$ International Conference on Rewriting Techniques and Applications"}
@string{rta7 = "Proc. of the $7^{th}$ International Conference on Rewriting Techniques and Applications"}
@string{rta8 = "Proc. of the $8^{th}$ International Conference on Rewriting Techniques and Applications"}




@Misc{Aub76,
  author = 	 "Raymond Aubin",
  title = 	 "Mechanizing structural induction",
  howpublished = "PhD Thesis, University of Edinburgh",
  year =	 1976
}


@Article{Aub79,
  author = 	 "Raymond Aubin",
  title = 	 "Mechanizing structural induction",
  journal = 	 tcs,
  year =	 1979,
  volume =	 9,
  pages =	 "347--362"
}


@Book{Ave95,
  author = 	 "J{\"u}rgen Avenhaus",
  title = 	 "Reduktionssysteme",
  publisher = 	 spring,
  year = 	 1995,
  note =         "(German)",
  address =	 "Berlin Heidelberg"
}


@InCollection{AveMad90,
  author = 	 "J{\"u}rgen Avenhaus and Klaus Madlener",
  title = 	 "Term rewriting and equational reasoning",
  booktitle =	 "Formal Techniques in Artificial Intelligence",
  publisher =	 "North-Holland",
  year =	 1990,
  editor =	 "R.B. Banerji",
  pages =	 "1--43",
  address =	 "Amsterdam"
}


@TechReport{AveMad95,
  author =       "J{\"u}rgen Avenhaus and Klaus Madlener",
  title =        "Theorem Proving in Hierarchical Clausal Specifications",
  institution =  "Fachbereich Informatik",
  year =         1995,
  type =         "SEKI-Report",
  number =       "SR-95-14",
  address =      "Universit{\"a}t Kaiserslautern, Germany"
}


@InCollection{AveMad97,
  author = 	 "J{\"u}rgen Avenhaus and Klaus Madlener",
  title = 	 "Theorem Proving in Hierarchical Clausal Specifications",
  booktitle =	 "Advances in Algorithms, Languages, and Complexity",
  publisher =	 "Kluwer Academic Press",
  year =	 1997,
  editor =	 "Ding{-Z}hu Du and Ker{-I} Ko",
  pages =	 "1--52"
}


@InProceedings{Bac88,
  author =       "Leo Bachmair",
  title = 	 "Proof by consistency in equational theories",
  booktitle =    lics3,
  year = 	 1988,
  pages =        "228--233"
}


@InProceedings{Bec92,
  author = 	 "Klaus Becker",
  title = 	 "Semantics for Positive/Negative Conditional Rewrite Systems",
  booktitle =	 ctrs3,
  year =	 1992,
  editor =	 "M. Rusinowitch and J.L. Remy",
  volume =	 656,
  series =	 lncs,
  pages =	 "213-225",
  publisher =	 spring
}


@Article{BerKlo86,
  author = 	 "J. A. Bergstra and J. W. Klop",
  title = 	 "Conditional Rewrite Rules: Confluence and Termination",
  journal = 	 "Journal of Computer and System Science",
  year =	 1986,
  volume =	 32,
  pages =	 "323-362"
}


@InProceedings{BevLew90,
  author = 	 "Eddy Bevers and Johan Lewi",
  title = 	 "Proof by Consistency in Conditional Equational Theories",
  booktitle =	 ctrs2,
  year =	 1990,
  editor =	 "S. Kaplan and M. Okada",
  volume =	 516,
  series =	 lncs,
  pages =	 "194--205",
  publisher =	 spring
}


@InCollection{BibEde93,
  author = 	 "Wolfgang Bibel and Elmar Eder",
  title = 	 "Methods and Calculi for Deduction",
  booktitle =	 "Handbook of Logic in Artificial Intelligence and Logic Programming",
  publisher =	 "Oxford University Press, Oxford",
  year =	 1993,
  editor =	 "Dov M. Gabbay and C. J. Hogger and J. A. Robinson",
  volume =	 1,
  chapter =	 3,
  pages =	 "67--182"
}


@InProceedings{BHHW86,
  author = 	 "Susanne Biundo and Birgit Hummel and Dieter Hutter and
                  Christoph Walther",
  title = 	 "The Karlsruhe Induction Theorem Proving System",
  booktitle =	 cade8,
  editor =	 "J{\"o}rg H. Siekmann",
  volume =	 230,
  series =	 lncs,
  pages =	 "672--674",
  year =	 1986,
  publisher =	 spring
}


@InProceedings{BouRus93,
  author = 	 "Adel Bouhoula and Micha{\"e}l Rusinowitch",
  title = 	 "Automatic Case Analysis in Proof by Induction",
  booktitle =	 ijcai13,
  year =	 1993,
  editor =	 "Ruzena Bajcsy",
  volume =	 1,
  pages =	 "88--94",
  publisher =	 "Morgan Kaufmann Publishers Inc."
}


@Article{BouRus95,
  author = 	 "Adel Bouhoula and Micha{\"e}l Rusinowitch",
  title = 	 "Implicit Induction in Conditional Theories",
  journal = 	 jar,
  year =	 1995,
  volume =	 14,
  pages =	 "189--235"
}


@Article{Bou96,
  author = 	 "Adel Bouhoula",
  title = 	 "Using induction and rewriting to verify and complete
                  parameterized specifications",
  journal = 	 tcs,
  year =	 1996,
  volume =	 170,
  pages =	 "245--276"
}


@Book{BoyMoo79,
  author = 	 "Robert S. Boyer and J Strother Moore",
  title = 	 "A Computational Logic",
  publisher = 	 "Academic Press",
  year = 	 1979,
  address =	 "New York"
}


@Book{BoyMoo88,
  author = 	 "Robert S. Boyer and J Strother Moore",
  title = 	 "A Computational Logic Handbook",
  publisher = 	 "Academic Press",
  year = 	 1988,
  address =	 "New York"
}


@InProceedings{BoyMoo90,
  author = 	 "Robert S. Boyer and J Strother Moore",
  title = 	 "A Theorem Prover for a Computational Logic",
  editor =	 "M. E. Stickel",
  volume =	 449,
  series =       lncs,
  pages =   	 "1--15",
  booktitle =	 cade10,
  year =	 1990,
  publisher =	 spring
}


@InProceedings{BroRedHas94,
  author = 	 "Francois Bronsard and Uday S. Reddy and Robert W. Hasker",
  title = 	 "Induction using Term Orderings",
  booktitle =	 cade12,
  year =	 1994,
  editor =	 "Alan Bundy",
  volume =	 814,
  series =	 lnai,
  pages =	 "102--117",
  publisher =	 spring
}


@InProceedings{BvHHS90,
  author = 	 "Alan Bundy and Frank van Harmelen and Christian Horn and Alan Smaill",
  title = 	 "The {O}yster-{C}lam system",
  editor =	 "M. E. Stickel",
  volume =	 449,
  series =       lncs,
  pages =   	 "647--648",
  booktitle =	 cade10,
  year =	 1990,
  publisher =	 spring
}


@Article{BSvHIS93,
  author = 	 "Alan Bundy and Andrew Stevens and Frank van Harmelen and Andrew Ireland and Alan Smaill",
  title = 	 "Rippling: a heuristic for guiding inductive proofs",
  journal =	 jai,
  year =	 1993,
  volume =	 62,
  pages =	 "185--253"
}


@Book{Coh65,
  author = 	 "P. M. Cohn",
  title = 	 "Universal Algebra",
  publisher = 	 "D. Reidel Publishing Company",
  year = 	 1965
}


@Book{Con86,
  author = 	 "Robert L. Constable",
  title = 	 "Implementing Mathematics with the {N}uprl Proof
                  Development System",
  publisher = 	 "Prentice-Hall",
  year = 	 1986,
  address =	 "Englewood Cliffs, NJ"
}


@Article{DeRKro76,
  author = 	 "F. DeRemer and H.H.\ Kron",
  title = 	 "Programming-in-the-Large versus Program\-ming-in-the-Small",
  journal = 	 "IEEE Transactions on Software Engineering",
  year =	 1976,
  volume =	 2,
  pages =	 "80-86"
}


@Article{Der87,
  author = 	 "Nachum Dershowitz",
  title = 	 "Termination of Rewriting",
  journal =	 jsc,
  year =	 1987,
  volume =	 3,
  pages =	 "69--116"
}



@InCollection{DerJou90,
  author = 	 "Nachum Dershowitz and Jean-Pierre Jouannaud",
  title = 	 "Rewrite Systems",
  booktitle =	 "Handbook of Theoretical Computer Science B: Formal Methods
                  and Semantics",
  publisher =	 "Elsevier Science Publishers B. V.",
  year =	 1990,
  editor =	 "J. van Leeuwen",
  chapter =	 6,
  pages =	 "243--320",
  address =	 "Amsterdam"
}


@Article{DerJou91,
  author = 	 "Nachum Dershowitz and Jean-Pierre Jouannaud",
  title = 	 "Notations for Rewriting",
  journal =	 "Bulletin of the European Association for Theoretical Computer Science (EATCS)",
  year =	 1991,
  volume =	 43,
  pages =	 "162--172"
}



@inproceedings{DerOkaSiv88,
   author = {N. Dershowitz and M. Okada and G. Sivakumar},
   title = "Confluence of Conditional Rewrite Systems",
   booktitle = ctrs1,
   pages = "31--44",
   publisher = spring,
   series = lncs,
   volume = {308},
   year = {1988}
}


@Book{EhrMah85,
  author = 	 "Hartmut Ehrig and Bernd Mahr",
  title = 	 "Fundamentals of Algebraic Specification",
  volume =       1,
  publisher = 	 spring,
  year = 	 1985,
  address =	 "Berlin Heidelberg New York Tokyo"
}


@Misc{Emb95,
  author =       "Christian Embacher",
  title =        "Entwurf und {I}mplementierung eines prototypischen
                  {I}nduktionsbeweisers f{\"u}r positiv/negativ bedingte
                  {R}ewrite-{S}pezifikationen ---
                  eine softwaretechnische {R}ealisierung",
  howpublished = "Projektarbeit (German), Fachbe\-reich Informatik,
                  Universit{\"a}t Kaiserslautern, Germany",
  year         =  1995
}


@Misc{Emb98,
  author =       "Christian Embacher",
  title =        "Realisierung von {B}eweissteuerungsverfahren f{\"u}r
                  den induktiven {T}heorembeweiser {Q}uod{L}ibet",
  howpublished = "Diplomarbeit (German), Fachbereich Informatik,
                  Universit{\"a}t Kaiserslautern, Germany",
  year         =  1998
}


@InProceedings{GarGut90,
  author = 	 "Stephen J. Garland and John V. Guttag",
  title = 	 "An overview of {LP}, the {L}arch {P}rover",
  volume =	 355,
  series =	 lncs,
  pages =	 "137--151",
  booktitle =	 rta3,
  year =	 1989,
  publisher =	 spring
}


@TechReport{GarGut91,
  author =       "Stephen J. Garland and John V. Guttag",
  title =        "A Guide to {LP}, the {L}arch {P}rover",
  institution =  "DEC-SRC",
  year =         1991,
  type =         "Technical Report",
  number =       "82"
}


@InProceedings{GerNol97,
  author = 	 "Stefan Gerberding and J. Axel Noltemeier",
  title = 	 "Incremental Proof Planning by Meta-Rules",
  pages =	 "171--175",
  booktitle =	 "Proc. $10^{th}$ Florida Artificial Intelligence Research Symposium (FLAIRS-97)",
  year =	 1997,
  publisher =	 "ISBN 0-9620-1739-6",
  address =      "Daytona Beach"
}


@Book{GorMilWad79,
  author = 	 "M. J. Gordon and R. Milner and C. P. Wadsworth",
  title = 	 "Edinburgh {LCF}:
                  A Mechanized Logic of Computation",
  publisher = 	 spring,
  volume =	 78,
  series =	 lncs,
  year = 	 1979
}


@Book{GorMel93,
  author = 	 "M. J. C. Gordon and T. F. Melham",
  title = 	 "Introduction to {HOL} ---
                  A theorem proving environment for higher order logic",
  publisher = 	 "Cambridge University Press",
  year = 	 1993,
  address =	 "Cambridge"
}


@TechReport{Gra90,
  author =       "Bernhard Gramlich",
  title =        "Completion Based Inductive Theorem Proving:
                  A Case Study in Verifying Sorting Algorithms",
  institution =  "Fachbereich Informatik",
  year =         1990,
  type =         "SEKI-Report",
  number =       "SR-90-04",
  address =      "Universit{\"a}t Kaiserslautern, Germany"
}


@TechReport{GraLin91,
  author =       "B. Gramlich and W. Lindner",
  title =        "A Guide to {UNICOM}, an Inductive Theorem Prover Based
                  on Rewriting and Completion Techniques",
  institution =  "Fachbereich Informatik",
  year =         1991,
  type =         "SEKI-Report",
  number =       "SR-91-17",
  address =      "Universit{\"a}t Kaiserslautern, Germany"
}


@InProceedings{HuaZha92,
  author = 	 "Xin Hua and Hantao Zhang",
  title = 	 "{FRI}: Failure-Resistant Induction in {RRL}",
  editor =	 "D. Kapur",
  volume =	 607,
  series =	 lnai,
  pages =	 "691--694",
  booktitle =	 cade11,
  year =	 1992,
  publisher =	 spring
}


@InProceedings{Hut90,
  author = 	 "Dieter Hutter",
  title = 	 "Guiding Induction Proofs",
  editor =	 "M. E. Stickel",
  volume =	 449,
  series =       lncs,
  pages =   	 "147--161",
  booktitle =	 cade10,
  year =	 1990
}


@Article{Hut97,
  author = 	 "Dieter Hutter",
  title = 	 "Colouring Terms to Control Equational Reasoning",
  journal = 	 jar,
  year =	 1997,
  volume =	 18,
  pages =	 "399--442"
}


@InProceedings{HutSen96,
  author = 	 "Dieter Hutter and Claus Sengler",
  title = 	 "{INKA}: {T}he Next Generation",
  booktitle =	 cade13,
  year =	 1996,
  editor =	 "M.A. McRobbie and J.K. Slaney",
  volume =	 1104,
  series =	 lnai,
  pages =	 "288--292",
  publisher =	 spring
}


@Article{IreBun96,
  author =       "Andrew Ireland and Alan Bundy",
  title =        "Productive Use of Failure in Inductive Proof",
  journal = 	 jar,
  year =	 1996,
  volume =	 16,
  pages =	 "79--111"
}


@Book{Jal91,
  author = 	 "Pankaj Jalote",
  title = 	 "An Integrated Approach to Software Engineering",
  publisher = 	 spring,
  year = 	 1991,
  address =	 "New York"
}


@Article{Kap84,
  author = 	 "S. Kaplan",
  title = 	 "Conditional Rewrite Rules",
  journal =	 tcs,
  year =	 1984,
  volume =	 33,
  pages =	 "175--193"
}


@Article{KapNieMus94,
  author = 	 "Deepak Kapur and Xumin Nie and David R. Musser",
  title = 	 "An overview of the {T}ecton proof system",
  journal = 	 tcs,
  year =	 1994,
  volume =	 133,
  pages =	 "307--339"
}


@Article{KapSub96a,
  author = 	 "Deepak Kapur and M. Subramaniam",
  title = 	 "New Uses of Linear Arithmetic in Automated Theorem
		  Proving by Induction",
  journal = 	 jar,
  year =	 1996,
  volume =	 16,
  pages =	 "39--78"
}


@InProceedings{KapSub96b,
  author = 	 "Deepak Kapur and M. Subramaniam",
  title = 	 "Automating Induction over Mutually Recursive Functions",
  booktitle =	 "Proc. of the $5^{th}$ International Conference on
                  Algebraic Methodology and Software Technology",
  year =	 1996,
  editor =	 "Martin Wirsing and Maurice Nivat",
  volume =	 1101,
  series =	 lncs,
  pages =	 "117--131",
  publisher =	 spring
}


@InProceedings{KapSub96c,
  author = 	 "Deepak Kapur and M. Subramaniam",
  title = 	 "Lemma Discovery in Automating Induction",
  booktitle =	 cade13,
  year =	 1996,
  editor =	 "M.A. McRobbie and J.K. Slaney",
  volume =	 1104,
  series =	 lnai,
  pages =	 "538--552",
  publisher =	 spring
}


@TechReport{KueWir96,
  author =       "Ulrich K{\"u}hler and Claus-Peter Wirth",
  title =        "Conditional Equational Specifications of Data Types
                  with Partial Operations for Inductive Theorem Proving",
  institution =  fbi,
  year =         1996,
  type =         "SEKI-Report",
  number =       "SR-96-11"
}


@InProceedings{KueWir97,
  author = 	 "Ulrich K{\"u}hler and Claus-Peter Wirth",
  title = 	 "Conditional Equational Specifications of Data Types
                  with Partial Operations for Inductive Theorem Proving",
  editor =	 "H. Comon",
  volume =	 1232,
  series =	 lncs,
  pages =	 "38-52",
  booktitle =	 rta8,
  year =	 1997,
  publisher =	 spring
}


@Misc{Kue99,
  author =       "U. K{\"u}hler",
  title =        "A Tactic-Based Inductive Theorem Prover for Data Types
                  with Partial Operations",
  howpublished = "PhD Thesis, Fachbereich Informatik,
                  Universit{\"a}t Kaiserslautern, Germany",
  year         =  1999,
  note         =  "Forthcoming"
}


@Misc{Kueetal98,
  author =       "Ulrich K{\"u}hler and Christian Embacher and Robert Eschbach
                  and J{\"u}rgen Schumacher and Tobias Schmidt{-S}amoa
                  and Christof Sprenger",
  title =        "\ql",
  howpublished = "System-Dokumentation (German), Fachbereich Informatik,
                  Universit{\"a}t Kaiserslautern, Germany",
  year         =  1998
}


@InProceedings{MidZan94,
  author = 	 "Aart Middeldorp and Hans Zantema",
  title = 	 "Simple Termination Revisited",
  booktitle =	 cade12,
  year =	 1994,
  editor =	 "Alan Bundy",
  volume =	 814,
  series =	 lnai,
  pages =	 "451--465",
  publisher =	 spring
}


@InCollection{Mus89,
  author = 	 "David R. Musser",
  title = 	 "Automated Theorem Proving for Analysis and Synthesis of Computations",
  booktitle =	 "Current Trends in Hardware Verification and Automated Theorem Proving",
  publisher =	 spring,
  year =	 1989,
  editor =	 "G. Birtwistle and P. A. Subrahmanyam",
  pages =	 "440--464"
}


@Book{Pad88,
  author = 	 "Peter Padawitz",
  title = 	 "Computing in Horn Clause Theories",
  publisher = 	 spring,
  year = 	 1988,
  address =	 "Berlin Heidelberg"
}


@Book{Pea84,
  author = 	 "Judea Pearl",
  title = 	 "Heuristics: intelligent search strategies
                  for computer problem solving",
  publisher = 	 "Addison-Wesley",
  year = 	 1984,
  address =	 "Reading"
}


@article{Pla85,
   author = "David A. Plaisted",
   journal = "Information and Control",
   pages = "182--215",
   title = "Semantic Confluence Tests and Completion Methods",
   volume = 65,
   year = 1985
}


@InCollection{Pla93,
  author = 	 "David A. Plaisted",
  title = 	 "Equational Reasoning and Term Rewriting Systems",
  booktitle =	 "Handbook of Logic in Artificial Intelligence and Logic Programming",
  publisher =	 "Oxford University Press, Oxford",
  year =	 1993,
  editor =	 "Dov M. Gabbay and C. J. Hogger and J. A. Robinson",
  volume =	 1,
  chapter =	 5,
  pages =	 "273--364"
}


@InProceedings{Pro94,
  author = 	 "Martin Protzen",
  title = 	 "Lazy Generation of Induction Hypotheses",
  booktitle =	 cade12,
  year =	 1994,
  editor =	 "Alan Bundy",
  volume =	 814,
  series =	 lnai,
  pages =	 "42--56",
  publisher =	 spring
}


@InProceedings{Red90,
  author = 	 "Uday S. Reddy",
  title = 	 "Term Rewriting Induction",
  editor =	 "M. E. Stickel",
  volume =	 449,
  series =       lncs,
  pages =   	 "162--177",
  booktitle =	 cade10,
  year =	 1990
}


@Misc{Sch97,
  author =       "Tobias Schmidt{-S}amoa",
  title =        "Realisierung einer {T}aktik-basierten
                  {B}eweissteuerungs{\-}komponente f{\"u}r
                  den induktiven {T}heorembeweiser {Q}uod{L}ibet",
  howpublished = "Pro{\-}jektarbeit (German), Fachbereich Informatik,
                  Universit{\"a}t Kaisers{\-}lautern, Germany",
  year         =  1997
}


@Misc{SchKue97,
  author =       "J{\"u}rgen Schumacher and Ulrich K{\"u}hler",
  title =        "{XQL} --- A Graphical User Interface for the Inductive Theorem Prover \ql",
  howpublished = "Unpublished technical report, Fachbereich Informatik,
                  Universit{\"a}t Kaiserslautern, Germany",
  year         =  1997
}


@Misc{Spr96,
  author =       "Christof Sprenger",
  title =        "{\"U}ber die {B}eweissteuerung
                  des induktiven {T}heorem{\-}bewei{\-}sers {Q}uod{L}ibet",
  howpublished = "Diplomarbeit (German), Fachbereich Informatik,
                  Universit{\"a}t Kaisers{\-}lautern, Germany",
  year         =  1996
}


@InProceedings{Wal94a,
  author = 	 "Toby Walsh",
  title = 	 "A Divergence Critic",
  booktitle =	 cade12,
  year =	 1994,
  editor =	 "Alan Bundy",
  volume =	 814,
  series =	 lnai,
  pages =	 "14--28",
  publisher =	 spring
}


@InProceedings{Wal88,
  author = 	 "Christoph Walther",
  title = 	 "Argument Bounded Algorithms as a Basis
                  for Automated Termination Proofs",
  editor =	 "E. Lusk and R. Overbeek",
  volume =	 310,
  series =	 lncs,
  pages =	 "601-622",
  booktitle =	 cade9,
  year =	 1988,
  publisher =	 spring
}


@InCollection{Wal94b,
  author = 	 "Christoph Walther",
  title = 	 "Mathematical Induction",
  booktitle =	 "Handbook of Logic in Artificial Intelligence and Logic Programming",
  publisher =	 "Oxford University Press, Oxford",
  year =	 1994,
  editor =	 "Dov M. Gabbay and C. J. Hogger and J. A. Robinson",
  volume =	 2,
  chapter =	 "13",
  pages =	 "127--228",
}


@Book{Wec92,
  author = 	 "W. Wechler",
  title = 	 "Universal Algebra for Computer Scientists",
  publisher = 	 spring,
  year = 	 1992,
  address =	 "Berlin Heidelberg"
}


@Article{Wir71,
  author = "Niklaus Wirth",
  title  = "The Programming Language {P}ascal",
  journal =	 "Acta Informatica",
  year =	 1971,
  volume =	 1,
  pages =	 "35--63"
}


@InCollection{Wir90,
  author = 	 "Martin Wirsing",
  title = 	 "Algebraic Specification",
  booktitle =	 "Handbook of Theoretical Computer Science B: Formal Methods and Semantics",
  publisher =	 "Elsevier Science Publishers B. V.",
  year =	 1990,
  editor =	 "J. van Leeuwen",
  chapter =	 13,
  pages =	 "675--788",
  address =	 "Amsterdam"
}


@TechReport{Wir95,
  author =       "Claus-Peter Wirth",
  title =        "Syntactic Confluence Criteria for
                  Positive/Negative-Conditional Term Rewriting Systems",
  institution =  "Fachbereich Informatik",
  year =         1995,
  type =         "SEKI-Report",
  number =       "SR-95-09",
  address =      "Universit{\"a}t Kaiserslautern, Germany"
}


@Book{Wir97,
  author =       "Claus-Peter Wirth",
  title =        "Positive/Negative-Conditional Equations ---
                  A Con\-struc\-tor-Based Framework for Specification and
                  Inductive Theorem Proving",
  note = "PhD Thesis",
  publisher = 	 "Verlag Dr.\ Kova\v{c}",
  year = 	 1997
}


@InProceedings{WirBec95,
  author = 	 "Claus-Peter Wirth and Klaus Becker",
  title = 	 "Abstract Notions and Inference Systems for Proofs by Mathematical Induction",
  booktitle =	 ctrs4,
  year =	 1995,
  editor =	 "N. Dershowitz and N. Lindenstrauss",
  volume =	 968,
  series =	 lncs,
  pages =	 "353--373",
  publisher =	 spring
}


@InProceedings{WirGra94a,
  author = 	 "Claus-Peter Wirth and Bernhard Gramlich",
  title = 	 "On Notions of Inductive Validity for First-Order Equational Clauses",
  booktitle =	 cade12,
  year =	 1994,
  editor =	 "Alan Bundy",
  volume =	 814,
  series =	 lnai,
  pages =	 "162--176",
  publisher =	 spring
}


@Article{WirGra94b,
  author = "Claus-Peter Wirth and Bernhard Gramlich",
  title  = "A Constructor-Based Approach to Positive/ Negative-Conditional Equational Specifications",
  journal =	 jsc,
  year =	 1994,
  volume =	 17,
  pages =	 "51--90"
}


@TechReport{WirKue95,
  author =       "Claus-Peter Wirth and Ulrich K{\"u}hler",
  title =        "Inductive Theorem Proving in Theories Specified by
		  Positive/Negative-Conditional Equations",
  institution =  "Fachbereich Informatik",
  year =         1995,
  type =         "SEKI-Report",
  number =       "SR-95-15",
  address =      "Universit{\"a}t Kaiserslautern, Germany"
}


@InProceedings{ZhaKapKri88,
  author = 	 "Hantao Zhang and Deepak Kapur and M. S. Krishnamoorthy",
  title = 	 "A Mechanizable Induction Principle for Equatioal Specifications",
  editor =	 "E. Lusk and R. Overbeek",
  volume =	 310,
  series =	 lncs,
  pages =	 "162--181",
  booktitle =	 cade9,
  year =	 1988,
  publisher =	 spring
}


@InProceedings{ZhaHua92,
  author = 	 "Hantao Zhang and Xin Hua",
  title = 	 "Proving the Chinese Remainder Theorem by the Cover Set Induction",
  editor =	 "D. Kapur",
  volume =	 607,
  series =	 lnai,
  pages =	 "431--445",
  booktitle =	 cade11,
  year =	 1992,
  publisher =	 spring
}