@string{acm 	= "ACM"}
@string{ieee	= "IEEE"}
@string{springer= "Springer-Verlag"}
@string{elsevier= "Elsevier Science"}
@string{mitpress= "The MIT Press"}
@string{kluwer	= "Kluwer Academic Publishers"}
@string{cambridgepress = "Cambridge University Press"}

@string{aaecc   = "Applicable Algebra in Engineering, Communication and Computing"}
@string{acta 	= "Acta Informatica"}
@string{eatcs 	= "Bulletin of the European Association for Theoretical Computer Science"}
@string{crasp	= "Compte-rendus de L'Acad\'{e}mie des Sciences de Paris"}
@string{crin 	= "{C}entre de {R}echerche en {I}nformatique de {N}ancy"}
@string{cs 	= "Computing Surveys"}
@string{cj 	= "Computing Journal"}
@string{fgcs 	= "Future Generation Computer Systems"}
@string{ipl  	= "Information Processing Letters"}
@string{ic  	= "Information and Computation"}
@string{jacm 	= "J. of the Association for Computing Machinery"}
@string{toplas 	= "ACM Transactions on Programming Languages and Systems"}
@string{jar 	= "Journal of Automated Reasoning"}
@string{jcss 	= "Journal of Computer and System Sciences"}
@string{jlp 	= "J. Logic Programming"}
@string{jsc  	= "Journal of Symbolic Computation"}
@string{jsl     = "Journal of Symbolic Logic"}
@string{mi 	= "Machine Intelligence"}
@string{ngc 	= "New Generation Computing"}
@string{scp  	= "Science of Computer Programming"}
@string{siam 	= "SIAM Journal on Computing"}
@string{tcs 	= "Theoretical Computer Science"}
@string{ai 	= "Artificial Intelligence"}
@string{dm 	= "Discrete Mathematics"}
@string{dam 	= "Discrete Applied Mathematics"}
@string{bit 	= "BIT"}
@string{mst     = {Mathematical Systems Theory}}
@string{ieeese 	= "IEEE Transactions on Software Engineering"}
@string{lncs    = "Lecture Notes in Computer Science"} 
@string{lnai    = "Lecture Notes in Artificial Intelligence"}

@string{univiowa = "University of Iowa"}
@string{univill = "University of Illinois"}
@string{csill = "Department of Computer Science"}
@string{univkl = "University of Kaiserslautern"}
@string{univparissud = "Universit\'e Paris-Sud"}
@string{univmontrealconcordia = "Concordia University"}

@string{deptcsiowa = "Department of Computer Science, " # univiowa}
@string{deptcskl = "Fachbereich Informatik, " # univkl}
 
@TechReport{BB92:aquila,
  author = 	"Alessandro Berarducci and Corrado B{\"o}hm",
  title = 	"A Self-Interpreter of Lambda Calculus Having a Normal Form",
  institution = 	"Dip. di Matematica Pura ed Applicata, Universita di
                 L'Aquila",  
  year = 	"1992",
  type = 	"Rapporto tecnico",
  number = 	"16",
  month = 	oct
}

@book{O85:mit,
     author = "Michael J. O'Donnell",
     year = 1985,
     title = "Equational Logic as a Programming Language",
     publisher = mitpress,
     address = "Cambridge, MA"
}

@incollection{K92:ox,
     author = "Jan Willem Klop",
     year = 1992,
     title = "Term Rewriting Systems",
     booktitle = "Handbook of Logic in Computer Science",
     editor = "S. Abramsky and D. M. Gabbay and T. S. E. Maibaum",
     publisher = "Oxford University Press",
     volume = 2,
     chapter = 1,
     pages = "1--117",
     address = "Oxford"
}

@Book{K80:mct,
     author = "Jan Willem Klop",
     year = 1980,
     title = "Combinatory Reduction Systems",
     series = "Mathematical Centre Tracts",
	publisher = "Mathematisch Centrum",
     address = "Amsterdam",
     volume = 127
}

@Article{BL79:jacm,
	author = "Berry, G{\'e}rard and L{\'e}vy, Jean-Jacques",
	year = 1979,
	title = "Mimimal and Optimal Computations of Recursive Programs",
	journal = jacm,
	volume = 26,
	pages = "148--175"
}

@InProceedings{comon97lics,
  author =      "Hubert Comon and Florent Jacquemard",
  title =       "Ground Reducibility is {EXPTIME}-complete",
  crossref =    "lics97",
  pages =       "26--34",
}

@Article{ComonJacquemard2003,
  author =       "Hubert Comon and Florent Jacquemard",
  title =        "Ground Reducibility is {EXPTIME}-complete",
  journal =      ic,
  volume =       "187",
  number =       "1",
  pages =        "123--153",
  year =         "2003",
}

@article{KNZ87:acta,
     author = "Deepak Kapur and Paliath Narendran and Hantao Zhang",
     month = aug,
     year = 1987,
     title = "On sufficient completeness and related properties of term
                 rewriting systems", 
     journal = acta,
     volume = 24,
     number = 4,
     pages = "395--415"
}

@article{P85:ic,
     author = "David A. Plaisted",
     month = may # "/" # jun,
     year = 1985,
     title = "Semantic confluence tests and completion methods",
     journal = "Information and Control",
     volume = 65,
     number = "2/3",
     pages = "182--215"
}

@inproceedings{W94:lics,
 author = "Joe B. Wells",
 title = "Typability and Type Checking in the Second-Order
		{$\lambda$}-Calculus Are Equivalent and Undecidable",
 crossref = "lics94",
}

@Book{H90:aw,
  title =        "Logical Foundations of Functional Programming",
  publisher =    "Addison-Wesley",
  year =         "1990",
  editor =    "G{\'e}rard Huet",
  series =    "University of Texas at Austin Year of Programming",
     address = "Reading, MA"
}
@incollection{B91:hlcs,
     author = "Henk Barendregt",
	title = "Lambda calculi with types",
	year = 1991,
     booktitle = "Handbook of Logic in Computer Science",
     editor = "S. Abramsky and D. M. Gabbay and T. S. E. Maibaum",
     publisher = "Oxford University Press",
     address = "Oxford",
     note = "To appear"
}


@inproceedings{V89:lics,
	author = "Roel C. de Vrijer",
	title = "Extending the lambda calculus with surjective pairing is
        	         conservative", 
	crossref = "lics89",
	pages = "204--215",
}


@techreport{Mar93,
        author="M. Marchiori",
        title="Modularity of {UN}$^\rightarrow$ for left-linear Term Rewriting Systems",
        year=1994,
        report="Technical Report CS-R9433",
institution = {CWI},
address = "{A}msterdam"
}
@inproceedings{M89:rta,
     author = "Aart Middeldorp",
     title = "Modular Aspects of Properties of Term Rewriting Systems
                 Related to Normal Forms",
     crossref = "rta89",
     pages = "263--277",
}


@InProceedings{K91:rta,
author	= "G. Kucherov",
title	= "On relationship between term rewriting systems and regular tree
  		languages",
crossref = "rta91",
}

@InProceedings{HH92:ctrs,
  author = 	"D. Hofbauer and M. Huber",
  title = 	"Computing linearizations using test sets",
  crossref =	"ctrs92",
  pages = 	"287--301"
}

@InProceedings{KT92:ctrs,
  author = 	"Gregory Kucherov and Mohamed Tajine",
  title = 	"Decidability of Regularity and Related Properties of Ground
                 	Normal Form Languages",
  pages = "272--286",
  crossref =	"ctrs92",
}

@article{KucherovTajine95ic,
  author    = {Gregory Kucherov and  Mohamed Tajine},
  title     = {Decidability of Regularity and Related Properties of Ground
               Normal Form Languages},
  journal   = ic,
  volume    = {118},
  number    = {1},
  year      = {1995},
  pages     = {91-100},
}

@Article{VG92:eatcs,
  author = 	"S. V{\'a}gv{\"o}lgyi and R. Gilleron",
  title = 	"For a rewrite system it is decidable whether the set
		 of irreducible, ground terms is decidable",
  journal = "Bulletin of the European Association for Theoretical Computer
                 Science", 
  year = 	"1992",
  volume = 	"48",
  pages = "197--209",
  month = 	oct
}
@inproceedings{DJK91:rta,
     author = "Nachum Dershowitz and Jean-Pierre Jouannaud and Jan Willem
                 Klop", 
     title = "Open Problems in Rewriting",
     crossref="rta91",
     pages = "445--456",
}

@inproceedings{G91:stacs,
	author = "R. Gilleron",
        title = "Decision Problems for Term Rewriting Systems and
                 Recognizable Tree Languages",
	crossref="stacs91"
}


@techreport{KM89:cwi,
	author = "Jan Willem Klop and Aart Middeldorp",
	title = "Sequentiality in Orthogonal Term Rewriting Systems",
	type = "Report",
	number = "CS-R8932",
	institution = "Centre for Mathematics and Computer Science",
	address = "Amsterdam",
	year = 1989
}

@article{KM91,
author	= "Jan Willem Klop and Aart Middeldorp",
title	= "Sequentiality in Orthogonal Term Rewriting Systems",
journal	= "Journal of Symbolic Computation",
volume	= 12,
year	= 1991,
pages	= "161-195",
}

@article{T87:ic,
	author = "S. Thatte", 
	title = "A Refinement of Strong Sequentiality for Term Rewriting 
with Constructors",
	journal = ic,
	volume = 72,
	pages = "46--65",
	year = 1987
}


@Article{AM96,
author	= "Sergio Antoy and Aart Middeldorp",
title	= "A Sequential Reduction Strategy",
journal	= "Theoretical Computer Science",
volume	= 165,
number	= 1,
year	= 1996,
pages	= "75--95",
}

@article{K89:apal,
	author = "J. R. Kennaway",
	title = "Sequential evaluation strategies for parallel-or and
related reduction systems",
	journal =  "Annals of Pure and Applied Logic",
	volume = 43,
	year = 1989,
	pages = "31--56"
}

@article{Mid93,
author	= "Aart Middeldorp",
title	= "Modular Properties of Conditional Term Rewriting Systems",
journal	= "Information and Computation",
volume	= 104,
number	= 1,
year	= 1993,
pages	= "110--158",
}

@phdthesis{M90:vrije,
	author = "Aart Middeldorp",
	title = "Modular Properties of Term Rewriting Systems",
	school = "Vrije Universiteit",
	address = "Amsterdam, The Netherlands",
	year = 1990
}


@inproceedings{DT90:lics,
        author = "Max Dauchet and Sophie Tison",
        title = "The Theory of Ground Rewrite Systems is Decidable",
	crossref = "lics90",
	pages = "242--248"
        }

@article{O87:tcs,
     author = "Michio Oyamaguchi",
     year = 1987,
     title = "The {Church-Rosser} property for ground term rewriting systems
                 is decidable", 
     journal = tcs,
     volume = 49,
     pages = "43--79",
     number = 1
}

@InProceedings{Okui:rta98,
  author   = "Satoshi Okui",
  title    = "Simultaneous Critical Pairs and {Church-Rosser} Property",
  crossref = "rta98",
  pages    = "2--16",
}

@InProceedings{OO97,
  author   = "Michio Oyamaguchi and Yoshikatsu Ohta",
  title	   = "A New Parallel Closed Condition for {C}hurch-{R}osser of
             	Left-Linear Term Rewriting Systems",
  crossref = "rta97",
  pages	   = "187--201",
}

@incollection{T88:pfgc,
	author = "Yoshihito Toyama",
	title = "Commutativity of Term Rewriting Systems",
	booktitle = "Programming of Future Generation Computers II",
	editor = " K. Fuchi and L. Kott",
	publisher = "North-Holland",
	pages = "393--407",
	year = "1988"
}

@article{H80:jacm,
     author = "G{\'e}rard Huet",
     month = oct,
     year = 1980,
     title = "Confluent reductions: {Abstract} properties and applications to
                 term rewriting systems", 
     journal = jacm,
     volume = 27,
     number = 4,
     pages = "797--821",
     annote = "Previous version in the {\em Proceedings of the Symposium on
                 Foundations of Computer Science}, Providence,
		RI, pp. 30-45 (October 1977)" 
}


@article{BK86:jcss,
     author = "J. A. Bergstra and Jan Willem Klop",
     year = 1986,
     title = "Conditional rewrite rules: {Confluency} and termination",
     journal = jcss,
     volume = 32,
     number = 3,
     pages = "323--362"
}


@techreport{V90:free,
	author ="Roel C. {de Vrijer}",
	title = "Unique normal forms for {Combinatory Logic} with Parallel
                 Conditional, a case study in conditional rewriting", 
	type = "Technical Report",
	institution = "Free University",
	address = "Amsterdam",
	year = 1990
}

@Article{yamada00tcs,
  author = "Toshiyuki Yamada and J{\"u}rgen Avenhaus and Carlos
            Lor\'{\i}a S\'aenz and Aart Middeldorp",
  title = "Logicality of Conditional Rewrite Systems",
  journal = tcs,
  volume = 236,
  number = "1--2",
  month = apr,
  year = 2000,
  pages = "209--232",
  url = "http://www1-c703.uibk.ac.at/\home{ami}/research/papers/tcs00.html"
}

@article{KV89:ic,
	author = "Jan Willem Klop and Roel C. {de Vrijer}",
	year = 1989,
	title = "Unique normal forms for lambda calculus with surjective
			pairing",
	journal = ic,
	volume = 80,
	pages = "97--113"
}

@inproceedings{KKSV91:rta,
	author = "J. R. Kennaway and Jan Willem Klop and
			M. R. Sleep and F. J. {de Vries}", 
	title = "Transfinite reductions in orthogonal term rewriting systems
                 ({Extended} abstract)",  
     	crossref = "rta91",
	pages = "1--12"
}

@article{M85:tcs,
     author = "Yves M{\'e}tivier",
     month = jan,
     year = "1985",
     title = "Calcul de longueurs de cha{\^\i}nes de r{\'e}{\'e}criture dans
                 le mono{\"\i}de libre", 
     journal = tcs,
     volume = "35",
     number = "1",
     pages = "71--87"
}


@InProceedings{W90:wert,
  author = 	"C. Wrathall",
  title = 	"Confluence of One-Rule {Thue} Systems",
  booktitle = 	"Proceedings of the First International Workshop on Word
                 Equations and Related Topics (Tubingen)",
  year = 	"1990",
  pages = 	"237--246",
  series = 	lncs,
  volume = 	572,
  publisher = 	springer,
  address = 	"Berlin"
}

@PhDThesis{K90:tuc,
  author = 	"W. Kurth",
  title = 	"{Termination und Konfluenz von Semi-Thue-Systems mit
     			nur einer Regel}",
  school = 	"Technische Universitat Clausthal",
  year = 	"1990",
  address = 	"Clausthal, Germany",
  note = 	"In German"
}

@InProceedings{C91:caap,
  author = 	"Anne-C\'ecile Caron",
  title = 	"Linear Bounded Automata and Rewrite Systems: {Influence} of
                 Initial Configurations on Decision Properties",
  booktitle = 	"Proceedings of the International Joint Conference on Theory
                 and Practice of Software Development, 
                 volume 1: Colloquium on Trees in Algebra and Programming
                 (Brighton, U.K.)", 
  month = apr,
  year = 	"1991",
  pages = 	"74--89",
  publisher = 	springer,
  address = 	"Berlin",
  series = lncs,
  volume = 493
}

@incollection{DJ90:htcs,
     author = "Nachum Dershowitz and Jean-Pierre Jouannaud",
     year = 1990,
     title = "Rewrite Systems",
     booktitle = "Handbook of Theoretical Computer Science",
     volume = "B: Formal Methods and Semantics",
     chapter = 6,
     pages = "243--320",
     editor = "J. van Leeuwen",
     publisher = "North-Holland",
     address = "Amsterdam"
}

@inproceedings{D89:rta,
     author = "Max Dauchet",
     title = "Simulation of {Turing} machines by a left-linear rewrite rule",
     crossref="rta89",
     pages = "109--120",
}




@techreport{C90:london,
	author = "E. A. Cichon",
	title = "Bounds on Derivation Lengths from Termination Proofs",
	type = "Technical Report",
	number = "CSD-TR-622",
	year = 1990,
	month = jun,
	institution = "Department of Computer Science, University of London",
	address = "Surrey, England"
}

@article{KP82:lms,
     author = "Laurie Kirby and Jeff Paris",
     year = 1982,
     title = "Accessible independence results for {Peano} arithmetic",
     journal = "Bulletin London Mathematical Society",
     volume = 14,
     pages = "285--293"
}

@Article{NieuwenhuisIPL93,
author	= " Robert Nieuwenhuis",
title	= "Simple {LPO} constraint solving methods",
journal	= "Information Processing Letters",
volume	= 47,
pages	= "65--69",
year	= 1993
}

@Article{ComonTreinen93:lri,
author  = "Hubert Comon and Ralf Treinen",
title   = "The First-Order Theory of Lexicographic Path Orderings is
                Undecidable",
journal = tcs,
volume  = 176,
number  = "1--2",
month   = apr,
year    = 1997,
pages   = "67--87"
}
  
@InProceedings{CCD93:rta,
  author = 	"Anne-C\'ecile Caron and Jean-Luc Coquid{\'e} and Max Dauchet",
  title = 	"Encompassment Properties and Automata with Constraints",
  crossref = 	"rta93",
  pages	=	"328--342",
}

@Article{V87:jacm,
  author = 	"K. N. Venkataraman",
  title = 	"Decidability of the Purely Existential Fragment of the Theory
                 of Term Algebras",
  journal = 	jacm,
  year = 	1987,
  volume = 	34,
  number = 	2,
  pages = 	"492--510"
}
@InProceedings{BC93:caap,
  author = 	"Alexandre Boudet and Hubert Comon",
  title = 	"About the Theory of Tree Embedding",
  crossref = 	"tapsoft93",
}

@Article{treinen92jsc,
  author = 	"Ralf Treinen",
  title = 	"A new method for undecidability proofs of first order
			theories",
  journal = 	jsc,
  year = 	"1992",
  volume = 	"14",
  number = 	"5",
  pages = 	"437--458",
  month = 	nov
}

@InProceedings{JO91:icalp,
  author =       "Jean-Pierre Jouannaud and Mitsuhiro Okada",
  title =        "Satisfiability of Systems of Ordinal Notations with the
                  Subterm Property is Decidable",
  booktitle = "Proceedings of the Eighteenth EATCS Colloquium on Automata,
                 Languages and Programming (Madrid, Spain)", 
  year =         "1991",
  editor = "J. Leach Albert and B. Monien and M. {Rodr\'{\i}guez} Artalejo",
  month =     jul,
  volume = 510,
  series = lncs,
  publisher = springer,
  address = "Berlin", 
  pages = "455--468"
}

@InProceedings{C90:lics,
  author = 	"Hubert Comon",
  title = 	"Solving Inequations in Term Algebras {(Preliminary version)}",
  crossref = 	"lics90",
  pages = 	"62--69",
}


@InProceedings{Marcinkowski:rta99,
  author	= "Jerzy Marcinkowski",
  title		= "Undecidability of the $\exists^*\forall^*$ Part of the
			Theory of Ground Term Algebra Modulo an {AC} Symbol",
  crossref	= "rta99",
  pages		= "92--102",
}

@InProceedings{LM93:stacs,
  author	= "D. Lugiez and J.-L. Moysset",
  title		= "Complement problems and tree automata in {AC}-like theories",
  booktitle	= "Proceedings of the  Symposium on Theoretical Aspects of
                 Computer Science (W{\"u}rzburg, Germany)",
  year		= 1993,
  publisher = 	springer,
  series = lncs,
  address = 	"Berlin"
}

@InProceedings{F93:rta,
  author	= "Maribel Fern{\'a}ndez",
  title		= "{AC}-Complement Problems: Validity and Negation
                 	Elimination", 
  crossref	= "rta93",
  pages		= "358--373",
}

@Article{comon93tcs,
  author        = "Hubert Comon",
  topics        = "teamp, constraints",
  title         = "Complete axiomatizations of some quotient term algebras",
  journal       = tcs,
  year          = 1993,
  volume        = 118,
  number        = 2,
  month         = sep
}

@Inproceedings{T90:fst,
	author  = "Ralf Treinen",
	title   = "A New Method for Undecidability Proofs of First Order Theories",
	booktitle = "Proceedings of the Tenth Conference on Foundations of Software
	                Technology and Theoretical Computer Science",
	editor  = "K. V. Nori and C. E. Veni Madhavan",
        volume = 472,
	publisher = springer,
        series = lncs,
	year    = 1990,
	pages   = "48--62"
}

@TechReport{W92:munster,
  author = 	"Andreas Weiermann",
  title = 	"Well-Rewrite Orderings and the Induced Recursive Path
                 Orderings", 
  institution = "Institut {f\"ur} Mathematische Logik und Grundlagenforschung",
  year = 	"1992",
  type = 	"Unpublished note"
}

@INPROCEEDINGS{L90:lics,
	AUTHOR = {Pierre Lescanne},
	TITLE = {Well rewrite orderings},
	crossref="lics90",
	PAGES = {239--256}
}


@InProceedings{LescanneALP92,
  AUTHOR = 	{Lescanne, Pierre},
  TITLE = 	"Termination of Rewrite Systems by Elementary Interpretations",
  crossref=	"alp92",
  PAGES = 	{21-36},
}

@techreport{L79:ltu,
     author = "Dallas S. Lankford",
     month = may,
     year = "1979",
     title = "On Proving Term Rewriting Systems are {Noetherian}",
     type = "Memo",
     number = "MTP-3",
     institution = "Mathematics Department, Louisiana Tech. University",
     address = "Ruston, LA",
     note = "Revised October 1979"
}

@article{BL87:scp,
     author = "Ahlem Ben Cherifa and Pierre Lescanne",
     month = oct,
     year = 1987,
     title = "Termination of Rewriting Systems by Polynomial Interpretations
                 and its Implementation", 
     journal = "Science of Computer Programming",
     volume = 9,
     number = 2,
     pages = "137--159"
}




@techreport{S91:bu,
	author = "Wayne Snyder",
	title = "A Note on the Complexity of Simplification Orderings",
	institution = "Boston University",
	address = "Boston, MA",
	year = 1991,
	type = "Technical Report",
        number = "TR 90--009",
        organization = ieee,
}

@article{KrN85:tcs,
     author = "M. S. Krishnamoorthy and P. Narendran",
     year = "1985",
     title = "On Recursive Path Ordering",
	journal = tcs,
	volume = 40,
	pages = "323--328"
}

@article{D87:jsc,
     author = "Nachum Dershowitz",
     month = "February/April",
     year = 1987,
     title = "Termination of Rewriting",
     journal = jsc,
     volume = 3,
     number = "1\&2",
     pages = "69--115",
     note = "Corrigendum: {\em 4}, 3 (December 1987), 409--410; reprinted in
                 {\em Rewriting Techniques and Applications}, J.-P. Jouannaud,
                 ed., pp. 69---115, Academic Press, 1987",
}


@article{B85:tcs,
 author = "G. Bauer",
 title = "{$n$-}Level Rewriting Systems",
 journal = tcs,
 volume = 40,
 year = 1985,
 pages = "85--99"
}
@techreport{DMT85:aero,
     author = "Nachum Dershowitz and Leo Marcus and Andrzej Tarlecki",
     month = dec,
     year = 1985,
     title = "Existence, Uniqueness, and Construction of Rewrite Systems",
     number = "ATR-85(8354)-7",
     institution = "Computer Science Laboratory, The Aerospace Corporation",
     address = "El Segundo, CA"
}

@Article{S89paa,
author	= "C. Squier",
title	= "Word problems and a homological finiteness condition for monoids",
journal	= "Journal of Pure and Applied Algebra",
year	= 1991,
}


@inproceedings{open3,
author = "Nachum Dershowitz and Jean-Pierre Jouannaud and Jan Willem Klop",
title  = "Problems in Rewriting {III}",
crossref="rta95",
pages="457--471",
}

@misc{freese93pc,
author  = "R. Freese",
title   = "personal communication",
year    = 1993,
}

@inproceedings{jm89:disco,
        author = "Jean-Pierre Jouannaud and Claude March{\'e}",
        title = "Completion Modulo Associativity, Commutativity and Identity",
        booktitle = "Proceedings of the International Symposium on the Design
                 and Implementation of Symbolic Computation Systems (Capri,
                 Italy)", 
        year = 1990,
        editor = "Alfonso Miola",
        volume = 429,
       series = lncs,
        publisher = springer,
        address = "Berlin", 
   pages = "111--120",
        month = apr
}
@inproceedings{BPW89,
        author = "Timothy Baird and Gerald Peterson and Ralph Wilkerson",
        title = "Complete Sets of Reductions Modulo {Associativity,
                 Commutativity and Identity}",
     	crossref="rta89",
        pages = "29--44"
        }

@article{JK86:siam,
     author = "Jean-Pierre Jouannaud and H{\'e}l{\`e}ne Kirchner",
     month = nov,
     year = "1986",
     title = "Completion of a set of rules modulo a set of equations",
     journal = siam,
     volume = "15",
     pages = "1155--1194",
}

@article{PS81:jacm,
     author = "Gerald E. Peterson and Mark E. Stickel",
     month = apr,
     year = "1981",
     title = "Complete sets of reductions for some equational theories",
     journal =jacm,
     volume = "28",
     number = "2",
     pages = "233--264"
}


@PhDThesis{Devie-thesis,
  author        = "Herv{\'e} Devie",
  title         = "Une approche alg{\'e}brique de la
                 r{\'e}{\'e}criture de preuves {\'e}quationnelles et
                 son application {\`a} la d{\'e}rivation de
                 proc{\'e}dures de compl{\'e}tion",
  school = 	univparissud,
  address =     "Orsay, France",
  year          = 1991, 
  month         = oct,
}

@InProceedings{bofill:lics99,
  author	= "Miquel Bofill and Guillem Godoy and Robert Nieuwenhuis
			and Albert Rubio",
  title		= "Paramodulation with Non-Monotonic Orderings",
  crossref	= "lics99",
  ftp		= "http://www-lsi.upc.es/~roberto/papers/sf.ps.gz"
}


@inproceedings{sattler95,
 author = "Andrea Sattler-Klein",
 title = "About Changing the Ordering During {Knuth-Bendix} Completion",
	booktitle = "Proceedings of the Symposium on Theoretical
                 Aspects of Computer Science", 
 pages = "175--186",
 year = 1994
}
 
@article{H81:jcss,
     author = "G{\'e}rard Huet",
     year = 1981,
     title = "A complete proof of correctness of the {Knuth-Bendix}
                 completion algorithm", 
     journal = "J. Computer and System Sciences",
     volume = 23,
     number = 1,
     pages = "11--21"
}


@inproceedings{KN85:ijcai,
     author = "Deepak Kapur and Paliath Narendran",
     month = aug,
     year = 1985,
     title = "An equational approach to theorem proving in first-order
                 predicate calculus", 
     booktitle = "Proceedings of the Ninth International Joint Conference on
                 Artificial Intelligence", 
     address = "Los Angeles, CA",
     pages = "1146--1153"
}

@inproceedings{BD87:lics,
     author = "Leo Bachmair and Nachum Dershowitz",
     title = "Inference Rules for Rewrite-Based First-Order Theorem Proving",
     crossref = "lics87",
     pages = "331--337"
}

@techreport{Z91:iowa,
   author = "Hantao Zhang",
   year = 1991,
   title = "A New Strategy for the {Boolean} Ring Based Approach
			to First Order Theorem Proving",
   type = "Technical Report",
   institution = deptcsiowa,
}

@techreport{MS88:seki,
     author = "J{\"u}rgen M{\"u}ller and Rolf Socher-Ambrosius",
     year = "1988",
     title = "Topics in completion theorem proving",
     type = "SEKI-Report",
     number = "SR-88-13",
     institution = deptcskl,
     address = "Kaiserslautern, West Germany",
     note = "To appear in {\em J. of Symbolic Computation}"
}

@article{H85:ai,
     author = "Jieh Hsiang",
     month = mar,
     year = 1985,
     title = "Refutational theorem proving using term-rewriting systems",
     journal = ai,
     volume = 25,
     pages = "255--300"
}


@phdthesis{Bronsard-thesis,
	Author = "Bronsard, Francois",
	Title = "Using Term Orders to Control Deductions",
	school = univill,
	Note = "Forthcoming",
	Year = 1995
}

@InProceedings{Bronsard-Reddy-reduction,
  author   = "Bronsard, F. and Reddy, U. S.",
  title    = "Reduction Techniques for First-Order Reasoning",
  pages    = "242--256",
  crossref = "ctrs92",
}

@inproceedings{BR90:lncs,
  author   = "Bronsard, Francois and Reddy, Uday S.",
  title    = "Conditional rewriting in {Focus}",
  crossref = "ctrs91",
}

@InProceedings{NO90:concordia,
  author = 	"Robert Nieuwenhuis and Fernando Orejas",
  title = 	"Clausal Rewriting",
  booktitle =   "Extended Abstracts of the Second International Workshop on
                 Conditional and Typed Rewriting Systems", 
  year = 	1990,
  editor = 	"S. Kaplan and M. Okada",
  publisher = 	univmontrealconcordia,
  pages     = "81--88",
  address = 	"Montreal, Canada",
  month = 	jun,
  note     = "Revised version to appear in {\em Lecture Notes in Computer
                 Science}, Springer-Verlag, Berlin" 
}

@Article{schmidt-schauss:jsc97,
  author        = "Manfred Schmidt-Schau{\ss}",
  title		= "A Unification Algorithm for Distributivity and a
			Multiplicative Unit",
  journal	= jsc,
  year		= 1997,
  pages		= "315--344",
  volume	= 22,
  number	= 3,
}

@TechReport{schmidt-schauss94a,
  author        = "Manfred Schmidt-Schau{\ss}",
  title         = "Unification of Stratified Second-Order Terms",
  institution   = "Fachbereich Informatik, Universit{\"a}t Frankfurt",
  year          = 1994,
  type          = "Research Report",
  number        = "12/94",
  address       = "Germany",
  month         = dec
}

@InProceedings{contejean93pc,
  author =       "Evelyne Contejean",
  title =        "Solving Linear {Diophantine} Constraints Incrementally",
  crossref =     "iclp93",
  pages =        "532--549",
  url =          "http://www.lri.fr/~contejea/iclp93.html",
}
  
@phdthesis{contejean92these,
  author        = "Evelyne Contejean",
  topics        = "unification, teamp",
  title         = "El{\'e}ments pour la D{\'e}cidabilit{\'e} de
                 	l'Unification modulo la Distributivit{\'e}",
  school  	= univparissud,
  address 	= "Orsay, France",
  year          = 1992,
  month         = apr
}

@InProceedings{contejean93icalp,
  author =       "Evelyne Contejean",
  title =        "A Partial Solution for {D}-unification based on a Reduction
                  to {AC1}-unification",
  pages =        "621--632",
  booktitle = 	"Proceedings of the EATCS International Conference on
                 	Automata, Languages and Programming", 
  year =         1993,
  publisher =    springer,
  address =      "Lund, Sweden",
  month =        jul,
  url =          "http://www.lri.fr/~contejea/icalp93.html"
}

@Article{tiden87jsc,
  author        = "Erik Tiden and Stefan Arnborg",
  title         = "Unification Problems with One-Sided Distributivity",
  journal       = jsc,
  year          = 1987,
  volume        = 3,
  pages         = "183-202"
}


@incollection{JK91:mit,
	author = "Jean-Pierre Jouannaud and Claude Kirchner",
	title = "Solving Equations in Abstract Algebras:  {A}
			Rule-Based Survey of Unification",
        editor = "Jean-Louis Lassez and Gordon Plotkin",
        publisher = mitpress,
        address = "Cambridge, MA",
        booktitle = "Computational Logic: Essays in Honor of Alan Robinson",
        year = 1991
}	
	
@incollection{KR89:reas,
     author = "St{\'e}phane Kaplan and Jean-Luc R{\'e}my",
     year = "1989",
     title = "Completion algorithms for conditional rewriting systems",
     volume = "2: Rewriting Techniques",
     booktitle = "Resolution of Equations in Algebraic Structures",
     editor = "H. A{\"\i}t-Kaci and M. Nivat",
     publisher = "Academic Press",
     address = "Boston",
     pages = "141--170"
}

@misc{comon93pc,
author	= "Hubert Comon",
title	= "Personal communication",
year	= 1993,
}


@inproceedings{BCD90:lics,
	author = "Alexandre Boudet and Evelyne Contejean and Herv{\'e} Devie",
	title = "A New {$AC$} Unification algorithm with an
		Algorithm for Solving Diophantine Equations",
	crossref = "lics90",
	pages = "289--299",
}

@article{F87:jsc,
     author = "Fran{\c c}ois Fages",
     month = jun,
     year = "1987",
     title = "Associative-commutative unification",
     journal = jsc,
     volume = "3",
     number = "3",
     pages = "257--275",
     note = "Previous version in the {\em Proceedings of the Seventh
                 International Conference on Automated Deduction},
		 Napa, CA, pp. 194-208 [May 1984]" 
}

@InProceedings{Vorobyov:TreeComplexity96,
  author  = "Sergei Vorobyov",
  title   = "An Improved Lower Bound for the Elementary Theories of Trees",
  crossref= "cade96",
  pages   = "275--287",
}

@inproceedings{M88:lics,
  author 	= "Michael J. Maher",
  title 	= "Complete axiomatizations of the algebras of the finite,
                        rational and infinite trees", 
  pages 	= "348--357",
  crossref= "lics88",
}

@InProceedings{T93:rta,
  author = "Tajine, Mohamed",
  title = " Negation Elimination for Syntactic Equational Formula",
  crossref = "rta93",
  pages = "316--327",
}

@article{LM87:jar,
        author = "J.-L. Lassez and K. G. Marriott",
        title = "Explicit Representation of Terms Defined by Counter
                Examples",
        journal = jar,
        year = 1987,
        volume = 3,
        number = 3,
        pages = "1--17",
        month = sep
        }

@phdthesis{C88:grenoble,
        author = "Hubert Comon",
        title = "Unification et Disunification: {T}h{\'e}orie et
                Applications",
        school = "Institut National Polytechnique de Grenoble",
        year = 1988,
	note = "In French",
        }


@inproceedings{BaaderSchulz-RTA-95,
        author = {Franz Baader and Klaus Schulz},
        title = {Combination of Constraint Solving Techniques:
                 {A}n Algebraic Point of View},
        crossref="rta95",
        pages  = {352--366},
}

@inproceedings{BaaderSchulz-CP-95,
        author = {Franz Baader and Klaus Schulz},
        title = {On the Combination of Symbolic Constraints,
                 Solution Domains, and Constraint Solvers},
        crossref="cp95",
}

@article{BaaderSchulz-TCS-98,
        author     = {Baader, Franz and Schulz, Klaus},
        title      = {Combination of Constraint Solvers for 
                      Free and Quasi-Free Structures},
        journal = {Theoretical Computer Science},
        note = {To appear.},
        year       = {1998}}

@InProceedings{DomenKRCADE94,
  author =       "E. Domenjoud and F. Klay and C. Ringeissen",
  title =        "Combination techniques for non-disjoint equational
                 	theories",
  crossref =     "cade94",
  pages =        "267--281",
}

@InProceedings{R92:lpar,
  author = 	"Christophe Ringeissen",
  title = 	"Unification in a Combination of Equational Theories with
                 Shared Constants and its Application to Primal Algebras",
  crossref = 	"lpar92",
}

@InProceedings{B92:cade,
  author = 	"Alexandre Boudet",
  title = 	"Unification in Order-Sorted Algebras with Overloading",
  crossref = 	"cade92",
}

@InProceedings{BS93:rta,
  author = 	"Franz Baader and Klaus Schulz",
  title = 	"Combination Techniques and Decision Problems for
                 Disunification",
  crossref=	"rta93",
  pages	= 	"301--315",
}

@InProceedings{BS92:cade,
  author = 	"Franz Baader and Klaus Schulz",
  title = 	"Unification in the Union of Disjoint Equational Theories:
                 {Combining} Decision Procedures",
  crossref=	"cade92",
}



@InProceedings{boudet94ccl,
  author =       "Alexandre Boudet and Evelyne Contejean",
  title =        "``{S}yntactic'' {AC}-Unification",
  crossref =	 "ccl94",
  pages =        "136--151",
  url =          "http://www.lri.fr/\home{contejea}/ccl94.html"
}

@incollection{JK90:mit,
  author        = "Jean-Pierre Jouannaud and Claude Kirchner",
  booktitle     = "Computational Logic: Essays in Honor of Alan Robinson",
  title         = "Solving equations in Abstract Algebras:
			A Rule-Based Survey of Unification",
  year          = 1991,
  publisher     = mitpress,
  editor        = "Jean-Louis Lassez and Gordon Plotkin"
}

@inproceedings{K86:lics,
     author = "Claude Kirchner",
     title = "Computing Unification Algorithms",
     crossref = "lics86",
     pages = "206--216",
}


@article{V84:tcs,
	author = "Venturini-Zilli, M.",
	year = 1984,
	title = "Reduction Graphs in the {Lambda Calculus}",
	journal = tcs,
	volume = 29,
	pages = "251--275"
}


@Article{KuchRusi94a,
  author = 	 {Gregory Kucherov and Micha\"el Rusinowitch},
  title = 	 "On the ground reducibility problem for word
		  rewriting systems with variables",
  journal = 	 "Information Processing Letters",
  year=          1994,
  note = 	 "To appear. Earlier version appeared in the
  Proceedings of 1994 ACM/SIGAPP Symposium on Applied Computing,
  Phoenix, AZ." 
}

@article{JK89:ic,
     author = "Jean-Pierre Jouannaud and Emmanuel Kounalis",
     year = "1989",
     title = "Automatic proofs by induction in equational theories without
                 constructors", 
     journal = ic,
     volume = 81,
     number = 1,
     pages = "1--33"
}

@techreport{KKSV90:cwi,
	author = "J. R. Kennaway and Jan Willem Klop and M. R. Sleep
		and F. J. {de Vries}", 
	title = "Transfinite reductions in orthogonal term rewriting systems",
	number = "CS-R9041",
	institution = "CWI",
	address = "Amsterdam",
	year = 1990
}

@Article{DKP91:tcs,
     author = "Nachum Dershowitz and St\'ephane Kaplan and David A. Plaisted",
     year = 1991,
     title = "Rewrite, Rewrite, Rewrite, Rewrite, Rewrite,\ldots",
     journal = tcs,
     volume = 83,
     number = 1,
     pages = "71--96",
}

@misc{BWerner,
  author        = "Benjamin Werner",
  topics        = logic,
  title         = "{\it M{\'e}ta-th{\'e}orie du Calcul des Constructions
			Inductives}", 
  howpublished  = "Th\`ese Univ. Paris VII, France",
  year          = 1994
}
@InProceedings{FernandezBarbaneraGeuvers:lics94,
  author        = "Franco Barbanera and Maribel Fern\'andez and
			Herman Geuvers",
  title         = "Modularity of Strong Normalization and Confluence
			in the $\lambda$-algebraic-cube",
  crossref     = "lics94",

}

@InProceedings{barbanera93tlca,
  author        = "Franco Barbanera and Maribel Fern{\'a}ndez",
  title         = "Combining first and higher order rewrite systems with
                 	type assignment systems", 
  crossref	= "tlca93",
}
@InProceedings{barbanera93icalp,
  author        = "Franco Barbanera and Maribel Fern{\'a}ndez",
  title         = "Modularity of termination and confluence in combinations
			of rewrite systems with {$\lambda_\omega$}",
  crossref	= "icalp93",
}

@inproceedings{JO91:lics,
  author =    "Jean-Pierre Jouannaud and Mitsuhiro Okada",
  title =     "Executable Higher-Order Algebraic Specification Languages",
  crossref =  "lics91",
  pages =     "350--361",
}

@inproceedings{D91:rta,
	author = "Daniel Dougherty",
	title = "Adding Algebraic Rewriting to the Untyped Lambda Calculus
                 (Extended Abstract)",
        crossref="rta91",
        pages = "37--48",
}

@article{DO90:tcs,
     author = "Nachum Dershowitz and Mitsuhiro Okada",
     year = 1990,
     title = "A Rationale for Conditional Equational Programming",
     journal = tcs,
     volume = 75,
     pages = "111--138",
}

@inproceedings{BG89:icalp,
	author = "Val Breazu-{T}annen and Jean Gallier",
	title = "Polymorphic Rewriting Conserves Algebraic Strong
			Normalization", 
	crossref="icalp89",
        pages = "137--150"
}

@article{barbanera90ijfcs,
  author        = "Franco Barbanera", 
  title         = "Combining Term Rewriting and Type Assignment Systems",
  journal       = "IJFCS",
  year          = 1990,
  volume        = 1,
  pages         = "165--184"
}


@Misc{Tison:habilitation,
author  = "Sophie Tison",
title   = "Automates Comme Outil De D\'ecision Dans Les Arbres",
year    = 1990,
month   = dec,
howpublished = "Dossier d'habilitation \`a diriger des recherches",
address = "Universit\'e des Sciences et Techniques de Lille, Lille, France",
note    = "In French",
}

@PhdThesis{Jacquemard:thesis,
  author = "Florent Jacquemard",
  title = "Automates d'arbres et R\'e\'ecriture de termes",
  school = "Universit\'e de Paris-Sud",
  year =         1996,
  note  = "In French."
}

@InProceedings{Vorobyov:rta97,
  author  = "Sergei Vorobyov",
  title   = "The First-Order Theory of One Step Rewriting in Linear
                Noetheran Systems is Undecidable",
  crossref = "rta97",
  pages   = "254--268",
}

@Inproceedings{Marcinkowski:rta97,
  author    = "Jerzy Marcinkowski",
  title     = "Undecidability of the First Order Theory of One-Step
                Right Ground Rewriting",
  crossref  = "rta97",
  pages     = "241--253",
}

@InProceedings{treinen97tapsoft,
   author       = "Franck Seynhaeve and Marc Tommasi and Ralf Treinen",
   title        = "Grid Structures and Undecidable Constraint Theories",
   crossref     = "tapsoft97",
   pages        = "357--368",
   year         = 1997,
}

@Article{seynhaeve01tcs,
  author     = "Franck Seynhaeve and Sophie Tison and Marc Tommasi and
                     Ralf Treinen", 
  title      = "Grid Structures and Undecidable Constraint Theories",
  journal    = tcs,
  volume     = 258,
  number     = "1--2",
  month      = may,
  year       = 2001,
  pages      = "453--490",
  ps         = "http://www.lsv.ens-cachan.fr/~treinen/publi/tcs-grid.ps.gz"
}

@InProceedings{Niehren:cade97,
author  = "Joachim Niehren and Manfred Pinkal and Peter Ruhrberg",
title   = "On Equality Up-to Constraints over Finite Trees, Context
                 Unification and One-Step Rewriting",
crossref= "cade97",
pages	= "34--48",
}
 


@book{B84:nh,
     author = "Henk Barendregt",
     year = "1984",
     title = "The Lambda Calculus, its Syntax and Semantics",
     publisher = "North-Holland",
     address = "Amsterdam",
     edition = "Second"
}

@article{Intrigila:IC97,
author	= "Benedetto Intrigila",
title	= "Non-existent Statman's Double Fixed Point Combinator
		Does Not Exist, Indeed",
journal	= ic,
volume	= 137,
number	= 1,
year	= 1997,
pages	= "35--40",
}

@TechReport{S91:cmu,
  author = 	"Richard Statman",
  title = 	"There is No Hyperrecurrent {S,K} Combinator",
  institution = 	"Department of Mathematics, Carnegie Mellon
                 University",
  address = "Pittsburgh, PA",
  type = 	"Research Report",
  number = "91--133",
  year = 1991
}
@InCollection{V80:cl,
  author = 	"A. Visser",
  title = 	"Numerations, Lambda Calculus, and Arithmetic",
  booktitle =   "Essays on Combinatory Logic, Lambda-Calculus, and
     Formalism",
  publisher = 	"Academic Press",
  year = 	"1980",
  editor = 	"Hindley and Seldin",
  pages = 	"259--284"
}


@TechReport{S92:inria,
  author = 	"Richard Statman",
  title = 	"A Short Note on a Problem of {Ray Smullyan}",
  institution = 	"INRIA-Rocquencourt",
  year = 	"1992",
  OPTaddress = 	"Le Chesnay, France",
  OPTmonth = 	sep
}




@MISC{Mano:93,
AUTHOR  = "Mano, Ken",
MONTH   = sep,
YEAR    = 1993,
NOTE    = "Personal communication"
}
@TECHREPORT{Oost:91,
AUTHOR  = "Oostrom, V. van",
TITLE   = "Confluence by Decreasing Diagrams",
TYPE    = "IR",
NUMBER  = 298,
MONTH   = aug,
INSTITUTION     = "Vrije Universiteit",
address = "Amsterdam, The Netherlands",
YEAR    = 1992,
NOTE    = "To appear in {\em Theoretical Computer Science}"
}

@phdthesis{Oost:94,
  author       = "Vincent van Oostrom",
  title        = "Confluence for Abstract and Higher-Order Rewriting",
  school       = "Vrije Universiteit, Amsterdam",
  year         = "1994",
  month        = mar,
  publisher    = "Copyprint 2000, Enschede",
}


@InProceedings{B90:cade,
  author = 	"Franz Baader",
  title = 	"Rewrite Systems for Varieties of Semigroups",
     booktitle = "Proceedings of the Tenth International Conference on
                 Automated Deduction (Kaiserslautern, West Germany)", 
     editor = "M. Stickel",
publisher = springer,
address = "Berlin",
  series = lncs,
  volume = 449,
  pages = "381--395",
  year = 	1990,
  month = 	jul
}


@inproceedings{Toyama94,
  author     = "Yoshihito Toyama and Michio Oyamaguchi",
  title      = "{Church-Rosser} Property and Unique Normal Form Property of
			Non-Duplicating  Term Rewriting Systems",
  crossref   = "ctrs94",
}
@article{Ohta94,
  author     = "Yoshikatsu Ohta and Michio Oyamaguchi and
			Yoshihito Toyama",
  title      = "On the {Church-Rosser} Property of Simple-Right-Linear
			Term Rewriting Systems",
  journal    = "Trans.  IEICE",
  year       = "to appear"
}
@Article{OO93:ieice,
  author = 	"Michio Oyamaguchi and Yoshikatsu Ohta",
  title = 	"On the Confluent Property of Right-Ground Term Rewriting
                 Systems ",
  journal = 	"Trans. IEICE",
  year = 	"1993",
  volume = 	"J76-D-I",
  pages = 	"39--45"
}

@inproceedings{D97:rta,
author = "Nachum Dershowitz",
title = "Innocuous Constructor-Sharing Combinations",
crossref = "rta97",
pages   = "202--216"
}

@article{RV80:jacm,
     author = "Jean-Claude Raoult and Jean Vuillemin",
     month = oct,
     year = "1980",
     title = "Operational and semantic equivalence between recursive
                 programs",
     journal = jacm,
     volume = "27",
     number = "4",
     pages = "772--796"
}

@InProceedings{Verma95,
  author	= "Rakesh M. Verma",
  title		= "Unique normal forms and confluence for rewrite systems",
  booktitle	= "Int'l Joint Conf. on Artificial Intelligence",
  year		= 1995,
  pages		= "362--368"
}

@TechReport{Verma96,
  author	= "Rakesh M. Verma",
  title		= "Unicity and Modularity of Confluence for Term
			Rewriting Systems",
  institution	= "University of Houston",
  year		= 1996
}

@PhDThesis{Geser:PhD,
  author	= "Alfons Geser",
  title		= "Relative Termination",
  school	= {qUniversit\"at Passau},
  address	= "Passau, Germany",
  year		= 1990
}
@InProceedings{Ohlebusch:caap94,
  author	= "Enno Ohlebusch",
  title		= "On the Modularity of Confluence of Constructor-Sharing Term
			Rewriting Systems",
  booktitle	= "19th Colloquium on Trees in Algebra and Programming",
  series	= "LNCS",
  volume	= 787,
  year		= 1994,
  pages		= "261-275",
  publisher	= "Springer-Verlag",
}

@inproceedings{MT91:rta,
     author = "Aart Middeldorp and Yoshihito Toyama",
     title = "Completeness of Combinations of Constructor Systems",
     crossref = "rta91",
     pages = "174--187",
}

@Article{KO92:tcs,
  author = 	"M. Kurihara and A. Ohuchi",
  title = 	"Modularity of Simple Termination of Term Rewriting Systems
                 with Shared Constructors",
  journal = 	tcs,
  year = 	"1992",
  volume = 	"103",
  pages = 	"273--282"
}
@article{T87:jacm,
     author = "Yoshihito Toyama",
     month = jan,
     year = "1987",
     title = "On the {Church-Rosser} Property for the Direct Sum of Term
                 Rewriting Systems", 
     journal = jacm,
     volume = "34",
     number = "1",
     pages = "128--143"
}

@InProceedings{Kri95,
author 	= "M.R.K. Krishna Rao",
title 	= "Semi-completeness of hierarchical and super-hierarchical
		 combinations of term rewriting systems",
booktitle = "Theory and practice of Software Development, TAPSOFT'95",
volume	= 915,
series	= "Lecture Notes in Computer Science",
pages	=  "379-393",
publisher =  "Springer-Verlag", 
year	= 1995}

@Article{Kri98,
author	= "M.R.K. Krishna Rao",
title	= "Modular Aspects of Term Graph Rewriting",
journal	= tcs,
volume  = 208,
number  = "1--2",
pages   = "59--86",
year    = 1998,
note	= "Special issue on Rewriting Techniques and Applications
 		conference RTA'96"
}

@article{Z94,
  author 	= {Hans Zantema},
  title 	= {Termination of term rewriting: interpretation and type
			elimination},
  journal 	= jsc,
  year 		= 1994,
  volume 	= 17,
  pages 	= {23-50}
}

@InProceedings{Z93,
  author	= "Hans Zantema",
  title		= "Type removal in term rewriting",
  pages		= "148--154",
  crossref	= "ctrs92",
}


@phdthesis{Oostrom-PhD,
  author="Oostrom, Vincent van",
  title="Confluence for Abstract and Higher-Order Rewriting",
  school="Vrije Universiteit",
  address={Amsterdam},
  year=1994
}

@article{Oostrom-TCS97,
  author="Oostrom, Vincent van",
  title="Developing Developments",
  journal=tcs,
  volume=175,
  year=1997,
  pages="159--181"
}

@phdthesis{Raamsdonk-PhD,
  author="Raamsdonk, Femke van",
  title={Confluence and Normalization for Higher-Order Rewriting},
  school={Vrije Universiteit},
  address={Amsterdam},
  year=1996
}

@InProceedings{Oost:Raam:94,
  author	= "Vincent van Oostrom and Femke van Raamsdonk",
  title	= " Weak orthogonality implies confluence: the higher-order case",
  pages	= "379--392",
  year	= 1994,
  editor	= "A. Nerode and Y. V. Matiyasevich",
  booktitle = "Third International Symposium on the Logical Foundations
		of Computer Science",
  address	= "{S}t. {P}etersburg, {R}ussia",
  month	= jul,
  publisher	= springer,
  series	= lncs,
  volume	= 813
}


@InProceedings{T93:tlca,
  author = 	"Masako Takahashi",
  title = 	"$\Lambda$-calculi with Conditional Rules",
  booktitle = 	"Proceedings of the International Conference on Typed Lambda
                 Calculi and Applications (Utrecht, The Netherlands)", 
  year = 	1993,
  editor = 	"M. Bezem and J. F. Groote",
  publisher = 	springer,
  address = 	"Berlin",
   series = lncs,
   volume = 664,
  pages = "406--417"
}
@inproceedings{N91:lics,
  author =    "Tobias Nipkow",
  title =     "Higher-Order Critical Pairs",
  crossref =  "lics91",
  pages = "342--349",
}

@ARTICLE{Mull:92,
AUTHOR  = "M{\"u}ller, Fritz",
TITLE   = "Confluence of the lambda calculus
           with left-linear algebraic rewriting",
JOURNAL = "Information Processing Letters",
PAGES   = "293--299",
VOLUME  = 41,
MONTH   = apr,
YEAR    = 1992,
PUBLISHER       = "North-Holland"
}

@inproceedings{O90:ieice,
 author = "Michio Oyamaguchi",
 title  = {On the Word Problem for Right-Ground Term-Rewriting Systems},
 booktitle = "Trans. IEICE",
 volume = "E73-5",
 pages = "718--723",
 year   = 1990
}

@article{DHLT90:ic,
  author = {Max Dauchet and Thierry Heuillard and Pierre Lescanne and
		Sophie Tison},
  title = {Decidability of the Confluence of Finite Ground Term
                 Rewriting Systems and of Other Related Term Rewriting Systems},
  journal = {Information and Computation},
  volume = 88,
  number = 2,
  month= oct,
  year = 1990,
  pages = "187--201"
}

@InProceedings{nieuwenhuis93rta,
  author	= "Robert Nieuwenhuis",
  title		= "A precedence-based total {AC}-compatible ordering",
  crossref	= "rta93",
  pages		= "374-388"
}

@InProceedings{CNNR:lics98,
  author	= "Hubert Comon and Paliath Narendran and Robert
			Nieuwenhuis and Micha{\"e}l Rusinowitch",
  title		= "Decision Problems in Ordered Rewriting",
  crossref	= "lics98",
}


@inproceedings{WZ95,
      author = {H. R. Walters and Hans Zantema},
      title = {Rewrite Systems for Integer Arithmetic},
      crossref = "rta95",
      pages	= "324--338",
}

@InProceedings{CohenW-RTA-91,
     author = {D. Cohen and Phil Watson},
     title = {An efficient representation of arithmetic for term rewriting},
     pages = {240-251},
     crossref="rta91",
}


@INPROCEEDINGS{BoudetCombination,
	AUTHOR = {Alexandre Boudet},
	TITLE = {Unification in combination of equational theories: {A}n
		 efficient algorithm},
	BOOKTITLE = "Proceedings of the Tenth International Conference on
	Automated Deduction (Kaiserslautern, Germany)",
	YEAR = {1990},
	PUBLISHER = springer,
	SERIES = lncs,
	VOLUME = {449}
}
@ARTICLE{SchmidtSchaussCombination,
	AUTHOR = {Manfred Schmidt-Schau{\ss}},
	TITLE = {Combination of Unification Algorithms},
	JOURNAL = jsc,
	YEAR = {1989},
	VOLUME = {8}
}


@INPROCEEDINGS{CharatonikPacholski-focs94,
     AUTHOR          = {Charatonik, W. and Pacholski, L.},
     TITLE           = {Set constraints with projections are in {NEXPTIME}},
     crossref	     = "focs94",
     PAGES           = {642--653},
}

@Techreport{aiken93cornell,
  author  = "A. Aiken and  D. Kozen and E. Wimmers",
  title  = "Decidability of systems of set constraints with negative
		constraints",
  institution = "Computer Science Department, Cornell University",
  year = "1993",
  type = "Technical Report",
  number = "93-1362"
}

@InProceedings{charatonik94lics,
  author        = "W. Charatonik and  L. Pacholski",
  title         = "Negative set constraints with equality",
  crossref	= "lics94",
  pages		= "128--136"
}

@InProceedings{gilleron93focs,
  author        = "R{\'e}my Gilleron and Sophie Tison and Marc Tommasi",
  title         = "Solving systems of set constraints with negated
                 	subset relationships",
  crossref	= "focs93",
  pages         = "372--380",
}

@InProceedings{GTT93:stacs,
  author	= "R{\'emy} Gilleron and Sophie Tison and Marc Tommasi",
  title		= "Solving Systems of Set Constraints using Tree Automata",
  crossref	= "stacs93",
}

@InProceedings{BGW93:lics,
  author = 	" Leo Bachmair and Harald Ganzinger and Uwe Waldmann",
  title = 	"Set  Constraints are the Monadic Class",
  crossref =	"lics93",
  pages =	"75--83",
}

@InProceedings{AW92:lics,
  author	= "A. Aiken and E. Wimmers",
  title		= "Solving Systems of Set Constraints",
  crossref	= "lics92",
  pages 	= "329--340",
}

@inproceedings{HJ90:lics,
  author	= "Nevin Heintze and Joxan Jaffar",
  title		= "A Decision Procedure for a Class of Set Constraints",
  crossref	= "lics90",
  pages 	= "42--51",
}


@InProceedings{BC92:alp,
  author = 	"Alexandre Boudet and Evelyne Contejean",
  title = 	"On $n$-Syntactic Equational Theories",
  booktitle = 	"Proceedings of the Third International Conference on
                 Algebraic and Logic Programming", 
  year = 	"1992",
  editor = 	"H. Kirchner and G. Levi",
  pages = 	"446--457",
  month = 	sep,
  volume =      632,
  series =      lncs,
  publisher =   springer,
  address =     "Pisa, Italy"
}


@Article{LMS:mst,
  author = 	"Igor Litovski and Yves M{\'e}tivier and Eric Sopena",
  title = 	"Definitions and Comparisons of Local Computations on Graphs",
  journal =     "Mathematical Systems Theory",
  year = 	"to appear",
  note = 	"Available as internal report 91-43 of LaBRI, University of Bordeaux 1"
}

@InProceedings{Thomas:tapsoft97,
  author	= "Wolfgang Thomas",
  title		= "Automata Theory On Trres And Partial Orders",
  booktitle	= "Theory and Practice of Software Development",
  series	= LNCS,
  volume	= 1214,
  year		= 1997,
  pages		= "20--38"
}


@InProceedings{   Bunke-Glauser-Tran:91,
  author        = {Horst Bunke and T. Glauser and T.-H. Tran},
  title         = {An Efficient Implementation of Graph Grammars Based on the
                  {RETE}-Matching Algorithm},
  editor        = {H. Ehrig and H.-J. Kreowski and G. Rozenberg},
  booktitle     = {Graph Grammars and Their Application to Computer Science},
  series        = {Lecture Notes in Computer Science},
  volume        = {532},
  pages         = {174--189},
  year          = {1991}
}


@Article{Courcelle:tcs94,
  author	= "Bruno Courcelle",
  title		= "Monadic-Second Order Graph Transductions: A Survey",
  journal	= tcs,
  volume	= 126,
  year		= 1994,
  pages		= "53--75"
}

@InCollection{Courcelle:HB97,
  author	= "Bruno Courcelle",
  title		= "The Expression Of Graph Properties And Graph Transformations
			 In Monadic Second-Order Logic",
  chapter	= 5,
  booktitle	= "Handbook of graph  grammars and computing by
			graph transformations, vol.~1: Foundations",
  editor	= "G. Rozenberg",
  publisher	= "World Scientific",
  address	= "New-Jersey, London",
  year		= 1997,
  pages		= "313--400",
}


@misc{RobertsonSeymour:96,
  author = "Neil Robertson and P. Seymour",
  title  = "Graph Minors 23: Nash-Williams' immersion conjecture",
  year	 = 1996,
  month	 = mar,
  howpublished = "Preprint"
}
  
@article{K60:tams,
     author = "Joseph B. Kruskal",
     month = may,
     year = 1960,
     title = "Well-quasi-ordering, the {Tree Theorem}, and {Vazsonyi's}
                 conjecture", 
     journal = "Transactions of the American Mathematical Society",
     volume = 95,
     pages = "210--225"
}

@Misc{RS82:osu,
author	= "Neil Robertson and P. D. Seymour",
title	= "Graph minors {IV. Tree-}width and well-quasi-ordering",
note	= "Submitted 1982; revised January 1986",
}


@InProceedings{P91:ctrs,
  author = 	"D. Plump",
  title = 	"Implementing Term Rewriting by Graph Reduction: {Termination}
                 of Combined  Systems",
  booktitle =   "Proceedings of the Second International Workshop on
                 Conditional and Typed Rewriting Systems (Montreal, Canada,
                 June 1990)",  
  year = 	1991,
  editor = 	"S. Kaplan and M. Okada",
  pages =       "307--317",
  volume = 516,
  series = lncs,
  publisher = springer,
  address = "Berlin"
}
@Article{HP91:rairo,
  author = 	"B. Hoffmann and D. Plump",
  title = 	"Implementing Term Rewriting by Jungle Evaluation",
  journal = 	"RAIRO Theoretical Informatics and Applications",
  year = 	"1991",
  volume = 	"25",
  number = 	"5",
  pages = 	"445--472"
}
@InProceedings{BEGKPS87:pal,
  author = 	"Henk Barendregt and M. C. J. D. {van Eekelen} and
			J. R. W. Glauert and J. R. Kennaway and
			M. J. Plasmeijer and M. R. Sleep",
  title = 	"Term Graph Rewriting",
  booktitle = 	"Proceedings of the European Workshop on Parallel
			Architectures and Languages",
  year = 	"1987",
  pages = 	"141--158",
  series =      lncs,
  publisher = 	springer,
  address = 	"Berlin",
  volume = 259
}


@InCollection{P93:tgr,
  author = 	"D. Plump",
  title = 	"Hypergraph Rewriting: {Critical} Pairs and Undecidability of Confluence",
  booktitle = 	"Term Graph Rewriting: Theory and Practice",
  publisher = 	"Wiley",
  year = 	"1993",
  editor = 	"M. R. Sleep and M. J. Plasmeijer and M. C. {van Eekelen}",
  chapter = 	"15",
  note = 	"To appear"
}


@Article{HW:ipl,
  author = 	"Philipp Hanschke and J{\"o}rg W{\"u}rtz",
  title =       "Satisfiability of the Smallest Binary Program",
  journal = 	ipl,
  year =        "1993",
  volume =      "45",
  number =      "5",
  pages =       "237--241",
  month =       apr,
}

@InProceedings{BHW92,
  author =      "Wolfgang Bibel and S. H{\"o}lldobler and J{\"o}rg W{\"u}rtz",
  title =       "Cycle Unification",
  crossref = 	"cade92",
  pages =       "94--108",
}

@misc{Devienne,
author	= "Phillipe Devienne",
title	= "Personal communication",
year	= 1993,
}

@TechReport{Rak96,
  author	= "Rakesh M. Verma",
  title		= "Unicity and Modularity of Confluence for Term Rewriting
			Systems",
  institution 	= "University of Houston",
  year		= 1996,
}

@InProceedings{Rak97,
  author	= "Rakesh M. Verma",
  title		= "Unique normal forms for nonlinear term rewriting systems:
			Root overlaps",
  booktitle	= "Symp. on Fundamentals of Computation Theory",
  publisher	= "Springer-Verlag",
  series	= LNCS,
  volume	= 1279,
  pages		= "452--462",
  month		= sep,
  year		= 1997
}

  
@InProceedings{ohlebusch94,
  author        = "Enno Ohlebusch",
  title         = "On the Modularity of Confluence of Constructor-Sharing
			Term Rewriting Systems",
  crossref	= "caap94",
}
 
@TECHREPORT{ManoOgawa:94, 
    AUTHOR = "K. Mano and M. Ogawa",
    TITLE = "A new proof of {Chew's} theorem", 
    INSTITUTION = "IPSJ PRG94-19-7",
    YEAR = 1994}

@InProceedings{C81:stoc,
  author = 	"Paul Chew",
  title = 	"Unique Normal Forms in Term Rewriting Systems with Repeated
                 Variables",
  booktitle = 	"Proceedings of the Thirteenth Annual Symposium on Theory of
                 Computing", 
  year = 	"1981",
  pages = 	"7--18",
  organization = 	"ACM"
}

@incollection{Ko86:lp,
     author = "William Kornfeld",
     year = 1986,
     title = "Equality for {Prolog}",
     booktitle = "Logic Programming: Functions, Relations, and Equations",
     editor = "D. DeGroot and G. Lindstrom",
     publisher = "Prentice-Hall",
     address = "Englewood Cliffs, NJ",
     pages = "279--293"
}
@TECHREPORT{OgawaOno:89,
    AUTHOR = "M. Ogawa and S. Ono",
    TITLE = "On the Uniquely Converging Property of Nonlinear Term
             Rewriting Systems",
    INSTITUTION = "IEICE COMP89-7",
    YEAR = 1989}
@INPROCEEDINGS{Martelli:84,
    AUTHOR = "A. Martelli and G. Rossi",
    TITLE = "Efficient unification with infinite terms in logic programming",
    BOOKTITLE = "International conference on fifth generation computer
                 systems",
    YEAR = 1984,
    PAGES = "202--209"}


@InProceedings{jouannaud94ctrs,
  author        = "Jean-Pierre Jouannaud and Walid Sadfi",
  title         = "Strong sequentiality of left-linear overlapping rewrite
                   	systems",
  crossref	= "ctrs94",
}

@InProceedings{toyama92,
  author        = "Yoshihito Toyama",
  title         = "Strong Sequentiality of Left Linear Overlapping
                 	Term Rewriting Systems",
  crossref	= "lics92",
}

@InCollection{HL91:mitb,
  author     = "G{\'e}rard Huet and Jean-Jacques L{\'e}vy",
  title      = "Computations in orthogonal rewriting systems, {II}",
  year       = "1991",
  booktitle  = "Computational Logic: Essays in Honor of Alan
                 Robinson",
  editor     = "Jean-Louis Lassez and Gordon Plotkin",
  chapter    = 12,
  pages      = "415--443",
  publisher  = mitpress,
  address    = "Cambridge, MA"
}	

@incollection{HL91:mit,
     author = "G{\'e}rard Huet and Jean-Jacques L{\'e}vy",
     title = "Computations in orthogonal rewriting systems, {I and II}",
	year = "1991",
        booktitle = "Computational Logic: Essays in Honor of Alan
                 Robinson",
        editor = "Jean-Louis Lassez and Gordon Plotkin",
        pages = "395--443",
        publisher = mitpress,
        address = "Cambridge, MA",
  note =         "This is a revision of \cite{HL79:inria}."
}	

@TechReport{HL79:inria,
  author	= "G\'erard Huet and Jean-Jacques L\'evy",
  title	        = "Call by need computations in non-ambiguous linear
                      term rewriting systems", 
  type	        = "Rapport Laboria",
  number	= 359,
  institution   = "Institut National de Recherche en Informatique
  		     et en Automatique",
  address	= "Le Chesnay, France",
  year	        = 1979,
  month	        = aug,
}

@TechReport{HL78:inria,
  author = "G{\'e}rard Huet and Dallas S. Lankford",
  month = mar,
  year = "1978",
  title = "On the Uniform Halting Problem for Term Rewriting Systems",
  type = "Rapport laboria",
  number = "283",
  institution = "Institut de Recherche en Informatique et en Automatique",
  address = "Le Chesnay, France"
}

@PhDThesis{Touzet:thesis,
  author	= "H{\'e}l{\`e}ne Touzet",
  title		= "Propri\'et\'es combinatoires pour la terminaison de
			 syst\`emes de r\'e\'ecriture",
  school	= "Universit\'e Henri Poincar\'e -- Nancy 1",
  address	= "Nancy, France",
  note		= "In French",
  month		= sep,
  year		= 1997,
  url		= "http://www.loria.fr/~ethouzet/these/these.ps.gz"
}

@InProceedings{touzet98,
  author = 	 {H{\'e}l{\`e}ne Touzet},
  title = 	 {Encoding the {H}ydra Battle as a Rewrite System},
  pages =        "267--276",
  crossref = 	 "mfcs98",
}

@InProceedings{touzet99rta,
  author =       "H{\'e}l{\`e}ne Touzet",
  title =        "A Characterization of Multiply Recursive Functions with
                     {H}igman's Lemma", 
  pages =        "163--174",
  crossref = 	 "rta99"
}

@ARTICLE{lepper:04,
  AUTHOR = {Ingo Lepper},
  TITLE = {Simply Terminating Rewrite Systems with Long Derivations},
  JOURNAL = {Archive for Mathematical Logic},
  VOLUME = 43,
  NUMBER = 1,
  PAGES = {1--18},
  YEAR = 2004
}


@PhDThesis{lepper:phd,
  author = "Ingo Lepper",
  title = "Simplification Orders in Term Rewriting",
  year = 2001,
  school = {Universit\"at M\"unster, Germany},
  note = {Available at 
           \ahrefurl{http://wwwmath.uni-muenster.de/logik/publ/diss/9.html}},
  url = "http://wwwmath.uni-muenster.de/logik/publ/diss/9.html",
}

@Misc{Weiermann:jsc,
 author          = "Andreas Weiermann",
 title           = "Bounding derivation lengths with functions from
                        the slow growing hierarchy",
 howpublished    = "Preprint M{\"{u}}nster",
 year            = 1993
}

@Article{Z4,
 author   = "Laurent Fribourg",
 title    = "A superposition oriented theorem prover",
 journal  = tcs,
 volume   = 35,
 year     = 1985,
 pages    = "161"
}

@Misc{Z3,
  author = "Jim Christian",
  title = "Problem Corner: An Experiment with {Grau's} Ternary {Boolean}
              Algebra",
  howpublished = "Submitted"
}

@Article{Z2,
 author   = "J. Zhang",
 title    = "A 3-place commutative operator from {TBA}",
 journal  = "{AAR} Newsletters",
 year     = "to appear"
}

@Misc{Z1,
  author = "Larry Wos",
  title  = "Automated Reasoning: 33 Basic Research Problems",
  pages = "156"
}

@PhDThesis{Rubio94,
  author  = "Albert Rubio",
  title	  = "Automated deduction with constrained clauses",
  school  = "Univ. de Catalunya",
  year	  = 1994,
}

@InProceedings{QuianWangLNCS845,
  author =       "Zheniu Qian and Kang Wang",
  title =        "Modular {AC}-Unification of Higher-Order Patterns",
  crossref =     "ccl94",
  pages =        "105--120",
}

@InCollection{miller91,
  author        = "Dale Miller",
  title         = "A logic programming language with lambda-abstraction,
                  function variables, and simple unification",
  booktitle     = "Extensions of Logic Programming",
  volume        = {690},
  series        = lncs,
  publisher     = springer,
  editor        = "P. Schroeder-Heister",
  year          = 1991
}

@InProceedings{boudet97cp,
  author =       "Alexandre Boudet and Evelyne Contejean",
  title =        "{AC}-Unification of Higher-order Patterns",
  crossref =     "cp97",
  url =          "http://www.lri.fr/\home{contejea}/cp97.html",
  ps =           "http://www.lri.fr/\home{contejea}/publis/cp97.ps.gz",
  pages =        "267--281"
}

@InProceedings{HR86:cade,
  author = {Jieh Hsiang and Micha\"el Rusinowitch},
  title = "A new method for establishing refutational completeness in
                 theorem proving", 
  crossref = "cade86",
  pages = "141--152",
}

@InProceedings{FZ93,
  author    = {M. C. F. Ferreira and Hans Zantema},
  title     = {Total Termination of Term Rewriting},
  crossref  = "rta93",
  pages     = {213--227},
  note      = "Extended version as \cite{FZ96}"
}

@Article{FZ96,
  author   = {M. C. F. Ferreira and Hans Zantema},
  title    = {Total Termination of Term rewriting},
  journal  = {Applicable Algebra in Engineering, Communication and
                Computing},
  year     = {1996},
  volume   = {7},
  number   = {2},
  pages    = {133-162}
}

@Article{D92,
  author  = "Max Dauchet",
  title	  = "Simulation of {T}uring machines by a regular rewrite rule",
  journal = tcs,
  volume  = 103,
  number  = 2,
  pages	  = "409--420",
  year	  = 1992,
}

@Article{lescanne94tcs,
  author  = "Pierre Lescanne",
  title	  = "On termination of one rule rewrite systems",
  journal = tcs,
  volume  = 132,
  number  = "1--2",
  pages	  = "395--401",
  year	  = 1994,
  month   = sep,
}

@InProceedings{geser97caap,
  author   = " Alfons Geser and Aart Middeldorp and Enno Ohlebusch
	        and Hans Zantema",
  title	   = "Relative Undecidability in the Termination Hierarchy of
		Single Rewrite Rules",
  pages	   = "237--248",
  crossref = "tapsoft97",
}

@TechReport{Z94open,
  author       = {Hans Zantema},
  title        = {Total termination of term rewriting is undecidable},
  institution  = {Utrecht University},
  year         = {1994},
  number       = {UU-CS-1994-55},
  month        = {December}
}

@Article{JK84:rairo,
  author  = "Jean-Pierre Jouannaud and H{\'e}l{\`e}ne Kirchner",
  year    = 1984,
  title   = "Construction d'un plus petit ordre de simplification",
  journal = "RAIRO Theoretical Informatics",
  volume  = 18,
  number  = 3,
  pages   = "191--207",
}

@Article{MG95,
  author  = {Aart Middeldorp and Bernhard Gramlich},
  title   = {Simple Termination is Difficult},
  journal = aaecc,
  year    = {1995},
  volume  = {6},
  number  = {2},
  pages   = {115--128}
}

@TechReport{DL94:hu,
  author =       "Nachum Dershowitz and Naomi Lindenstrauss",
  title =        "Abstract And-Parallel Machines",
  institution =  "Department of Computer Science, Hebrew University",
  year =         1994
}

@TechReport{BD92:uiuc,
  author = "Leo Bachmair and Nachum Dershowitz",
  title = "Equational Inference, Canonical Proofs, and Proof Orderings",
  type = "Report",
  number = "DCS-R-92-1746",
  month = apr,
  year = 1992,
  institution = csill # ", " # univill,
  address = "Urbana, IL"
}

@InProceedings{Munioz:lics96,
  author = "C{\'e}sar  Mu{\~n}oz",
  title  = "Confluence and Preservation of Strong Normalisation in
		an Explicit Substitutions Calculus (Extended Abstract)",
  crossref= "lics96",
  pages	= "440--447",
}

@TechReport{LescanneR94,
  author = {Lescanne, Pierre and Rouyer-Degli, J.},
  title  = {The Calculus of explicit substitutions $\lambda\upsilon$},
  institution = {INRIA-Lorraine},
  year = {1994},
  number = {RR-2222},
  month = jan
}

@InProceedings{Mellies95,
  author   = {Paul-Andr\'e Melli\`es},
  title    = {Typed $\lambda$-calculi with explicit substitutions may
			not terminate},
  crossref ="tlca95",
}

@TechReport{CurienHardinLevy92,
  author      = {Pierre-Louis Curien and Th\'er\`ese Hardin and
                        Jean-Jacques L{\'e}vy},
  title       = {Confluence properties of weak and strong calculi of
			explicit substitutions},
  institution = "Institut National de Rechereche en Informatique et
             	    en Automatique",
  type        = {RR},
  number      = {1617},
  address     = {Rocquencourt, France},
  year        = 1992,
  month       = feb
}

@Article{Makanin:77,
  author	= "G. S. Makanin",
  title		= "The Problem of Solvability of Equations in a Free
			Semi-Group",
  journal	= "Math. USSR Sbornik",
  volume	= 32,
  number	= 2,
  year		= 1977,
  pages	= "129--198",
}

@Article{Goldfarb:tcs81,
  author	= "Warren D. Goldfarb",
  title		= "The Undecidability of the Second-Order Unification
			Problem",
  journal	= tcs,
  volume	= 13,
  year		= 1981,
  pages		= "225--230",
}

@TechReport{Comon:rr699,
  author	= "Hubert Comon",
  title		= "Completion of Rewrite Systems with Membership Constraints",
  type		= "Rapport de Recherche",
  number	= 699,
  institution	= "L.R.I., Universit\'e de Paris-Sud",
  month		= sep,
  year		= 1991
}

@InProceedings{Comon:icalp92,
  author	= "Hubert Comon",
  title		= "Completion of Rewrite Systems with Membership Constraints",
  pages		= "392--403",
  crossref	= "icalp92",
}

@Article{Comon98ajsc,
  author	= "Hubert Comon",
  title		= "Completion of Rewrite Systems with Membership Constraints.
                   {P}art {I}: Deduction Rules",
  journal       = jsc,
  year          = 1998,
  volume        = 25,
  pages         = "397--419",
}

@Article{Comon98bjsc,
  author	= "Hubert Comon",
  title		= "Completion of Rewrite Systems with Membership Constraints.
                   {P}art {II}: Constraint Solving",
  journal       = jsc,
  year          = 1998,
  volume        = 25,
  pages         = "421--453",
}

@TechReport{Schauss:rr94-12,
  author	= "Manfred Schmidt-Schau\ss",
  title		= "Unification of Stratified Second-Order Terms",
  type		= "Internal Report",
  number	= "12/94",
  institution	= {Johann\--Wolfgang\--Goethe\--Universit\"at},
  address	= "Frankfurt, Germany",
  year		= "1994",
  url	  = "http://www.ki.informatik.uni-frankfurt.de/papers/schauss/D-uni-SO-9-95.ps.gz",
}

@InProceedings{schmidt-schauss:rta98,
  author	= "Manfred Schmidt-Schau{\ss} and Klaus Schulz",
  title		= "On the Exponent of Peridicity of Minimal Solutions
			of Context Equations",
  crossref	= "rta98",
  pages		= "61--75",
}

@InProceedings{Levy:rta96,
  author	= "Jordi Levy",
  title		= "Linear Second-Order Unification",
  pages		= "332--346",
  crossref	= "rta96",
}

@Article{LevyAgust:jsc96,
  author        = "Jordi Levy and Jaume Agust\'\i",
  title         = "Bi-rewriting Systems",
  journal       = jsc,
  year          = 1996,
  month         = sep,
  volume        = 22,
  number        = 3,
  pages         = "279--314",
}

@InProceedings{Schauss:cade99,
  author	= "Manfred Schmidt-Schau{\ss} and Klaus Schulz",
  title		= "Solvability of Context Unification with two Context
			Variables is Decidable",
  crossref	= "cade99",
  pages		= "67-81",
  note		= "Complete version as \cite{Schauss:cisrep99}",
}

@TechReport{Schauss:cisrep99,
  author	= "Manfred Schmidt-Schau{\ss} and Klaus Schulz",
  title		= "Solvability of Context Unification with two Context
			Variables is Decidable",
  institution 	= {CIS, Universit\"at M\"unchen},
  address 	= {M\"unchen, Germany},
  type 		= "CIS-Report",
  number 	= "98-114",
  year		= 1999,
  url="http://www.cis.uni-muenchen.de/pub/cis-berichte/CIS-Bericht-98-114.ps",
}

@InProceedings{Levy:rta00,
  author	= "Jordi Levy and Mateu Villaret",
  title		= "Linear Second-Order Unification and Context
			Unification with Tree-Regular Constraints",
  crossref	= "rta00",
  pages		= "156--171",
}

@Book{BoOt93,
  author    = "R. V. Book and Friedrich Otto",
  title     = "String-Rewriting Systems",
  publisher = springer,
  year      = 1993,
}

@Article{CRRT96,
  author    = "C. M. Campbell and E. F. Robertson and  N. Ru\u{s}kuc
			 and M. R. Thomas",
  title     = "On Subsemigroups and Ideals in Free Products of Semigroups.",
  journal   = "Int. J. of Algebra and Computation",
  volume    = 6,
  pages     = "571--591", 
  year      = 1996,
}

@Book{Eps92,
  author    = "D. B. A. Epstein",
  title     = "Word Processing In Groups",
  publisher = "XJones and Bartlett Publishers",
  year      =  1992,
}

@InCollection{Ger92a,
  author    = "S. M. Gersten",
  title     = "Dehn functions and l1-norms of finite presentations",
  pages     = "195--224",
  editor    = "G. Baumslag and C. F. Miller III",
  booktitle = "Algorithms and Classification in Combinatorial Group Theory",
  series    = "Math. Sciences Research Institute Publ.",
  volume    = 23,
  publisher = springer,
  year      =  1992,
}

@InCollection{Ger92b,
  author    = "S. M. Gersten",
  title     = "Problems on automatic groups",
  pages     = "225--232",
  editor    = "G. Baumslag and C. F. Miller III",
  booktitle = "Algorithms and Classification in Combinatorial Group Theory",
  series    = "Math. Sciences Research Institute Publ.",
  volume    = 23,
  publisher = springer,
  year      =  1992,
}

@InProceedings{KuMa89,
  author    = "N. Kuhn and Klaus Madlener",
  title     = "A method for enumerating cosets of a group presented
			by a canonical system",
  booktitle = "Proc. ISSAC'89",
  pages     = "338--350",
  publisher = acm,
  year      = 1989,
}

@InProceedings{otto:rta98,
  author    = "Friedrich Otto and Andrea Sattler-Klein and Klaus Madlener",
  title     = "Automatic Monoids Versus Monoids with Finite Convergent
  			Presentations",
  crossref  = "rta98",
  pages     = "32--46",
}

@InProceedings{Gutierrez:focs98,
  author	= {C. Guti\'errez},
  title		= "Satisfiability of Word Equations with Constants is in
			Exponential Space",
  crossref	= "focs98",
}

@InCollection{Dieckert:Makanin01,
  author	= "Volker Diekert",
  title		= "Makanin's Algorithm",
  url		= "http://www.informatik.uni-stuttgart.de/ifi/ti/makanin.ps",
  crossref      = "lothaire:words02",
  chapter       = 12,
  pages         = "387--442",
}

@InProceedings{Caron:rta99,
  author	= "Anne-C\'ecile Caron and Franck Seynhaeve and
			Sophie Tison and Marc Tommasi",
  title		= "Deciding the Satisfiability of Quantifier Free
			Formulae on One-Step rewriting",
  crossref	= "rta99",
  pages		= "103--117",
}

@InProceedings{Limet:rta99,
  author	= "S\'ebastien Limet and Pierre R\'ety",
  title		= "A New Result about the Decidability of the Existential
			One-Step Rewriting Theory",
  crossref	= "rta99",
  pages		= "118--132",
}

@InProceedings{Treinen:rta96,
  author        = "Ralf Treinen",
  title         = "The First-Order Theory of One-Step Rewriting is
                        Undecidable",
  crossref      = "rta96",
  pages         = "276--286",
  url  = "http://www.lsv.ens-cachan.fr/\home{treinen}/publi/rta96-rep.ps.gz",
}

@Article{treinen98tcs,
  author  = "Ralf Treinen",
  title   = "The First-Order Theory of Linear One-Step Rewriting
                    is Undecidable",
  journal = tcs,
  volume  = 208,
  number  = "1--2",
  pages   = "179--190",
  year    = 1998,
  month   = nov,
}

@InProceedings{comon:csl97,
  author   = "Hubert Comon and Yan Jurski",
  title    = "Higher-order matching and tree automata",
  crossref = "csl97",
  pages	   = {157--176},
}

@PhDThesis{Huet:these,
  author   = "G{\'e}rard Huet",
  title    = "R\'esolution d'\'equations dans les langages d'ordre
		$1,2,\ldots,\omega$",
  type	   = {Th\`ese d'\'Etat},
  school   = "Universit\'e Paris 7",
  address  = "Paris, France",
  year     = 1976
}

@Article{Dowek:apal93,
  author   = "Gilles Dowek",
  title    = "Third Order Matching Is Decidable",
  journal  = "Annals of Pure and Applied Logic",
  year     = 1993
}

@PhDThesis{Padovani:these,
  author   = "Vincent Padovani",
  title    = "Filtrage d'ordre sup\'erieure",
  type     = "PhD Thesis",
  school   = "Universit\'e de Paris 7",
  address  = "Paris, France",
  year     = 1996
}

@InProceedings{deGroote:rta00,
  author   = "Philippe de Groote",
  title    = "Linear Higher-Order Matching is {NP}-Complete",
  crossref = "rta00",
  pages    = "127--140"
}

@InProceedings{Wierzbicki:cade99,
  author   = "Tomasz Wierzbicki",
  title    = "Complexity of the Higher-Order Matching",
  crossref = "cade99",
  pages    = "82--96"
}

@InProceedings{Vorobyov:lics97,
  author   = "Sergei Vorobyov",
  title    = {The "Hardest" Natural Decidable Theory},
  crossref = "lics97",
  pages    = "294--305"
}

@InProceedings{Schubert:tapsoft97,
  author   = "Aleksy Schubert",
  title    = "Linear Interpolation for the Higher-Order Matching Problem",
  crossref = "tapsoft97",
  pages    = "441--452"
}


@techreport{ZG96,
  author 	= {Hans Zantema and Alfons Geser},
  title 	= {Non-looping rewriting},
  institution 	= {Utrecht University},
  year 		= 1996,
  number 	= {UU-CS-96-03},
  address 	= {Department of Computer Science},
  month 	= jan,
  note		= {Extended version to appear in {\it RAIRO Th\'eor. Inf}
			as "Non-looping string rewriting"},
}

@InProceedings{statman:rta2000,
  author   = "Rick Statman",
  title    = "On the Word Problem for Combinators",
  crossref = "rta00",
  pages    = "203--213"
}

@TechReport{Waldmann:report97,
  author        = "Johannes Waldmann",
  title         = "How to decide {S}",
  number        = "97/03",
  type          = "Forschungsergebnisse",
  year          = 1997,
  institution   = {Friedrich-Schiller-Universit\"at Jena, Fakult\"at
                   Mathematik}, 
  address	= "Jena, Germany",
}

@InProceedings{Waldmann:rta98,
  author        = "Johannes Waldmann",
  title         = "Normalisation of $S$-Terms is Decidable",
  crossref      = "rta98",
  pages         = "138--150"
}

@PhDThesis{Waldmann:phd,
  author        = "Johannes Waldmann",
  title         = "The Combinator {S}",
  school        = {Fakult\"at f\"ur Mathematik und Informatik of the
                   Friedrich-Schiller-Universit\"at Jena} ,
  address       = "Jena, Germany",
  year          = 1998,
  url           = "http://www.imn.htwk-leipzig.de/\home{waldmann}"
}


@InProceedings{dougherty:rta00,
  author    = "Dan Dougherty and Claudio Guti\'errez",
  title	    = "Normal Forms and Reduction for Theories of Binary Relations",
  crossref  = "rta00",
  pages	    = "95--109",
}

@Book{FreydScedrov:Allegories,
  author     = "Peter Freyd and Andre Scedrov",
  title	     = "Categories and Allegories",
  publisher  = "North-Holland",
  year	     = 1990,
  volume     = 39,
  series     = "North Holland Mathematical Library",
}

@inproceedings{barendregt:lambda75:open,
        author = "Henk Barendregt",
        title = "Open Problems",
        pages = "367--370",
        booktitle = "Lambda Calculus and Computer Science Theory",
        editor = "Corrado B{\"o}hm",
        year = 1975,
        publisher = springer,
        series = lncs,
        volume = 37,
}

@Article{GGL:SKIn,
  author = {Goguen, Healfdene and Goubault-Larrecq, Jean},
  title =  {Sequent Combinators: A {H}ilbert System for the Lambda Calculus}, 
  journal = {Mathematical Structures in Computer Science},
  year =   {2000},
  volume = {10},
  pages =  {1--79},
  postscript = "http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GogGou-MSCS2000.ps"
}

@InCollection{JGL:SKInT:conj,
  author = 	 {Goubault-Larrecq, Jean},
  title = 	 {Conjunctive Types and {SKInT}},
  booktitle = 	 {Proceedings of the TYPES'98 Workshop},
  publisher =	 springer,
  year =	 {1999},
  series =	 lncs,
  address =	 {Bad Irsee, Germany},
  postscript =   "http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-types98.ps"
}

@InProceedings{Ohlebusch97alp,
  author	= "Enno Ohlebusch",
  title		= "Conditional Term Graph Rewriting",
  pages		= "144--158",
  crossref	= "alp97",
  url		= "http://www.TechFak.uni-bielefeld.de/techfak/persons/enno/publications.html#peo",
}

@InProceedings{HermannKolaitis96cade,
  author   = {Miki Hermann and P. G. Kolaitis},
  title	   = {Unification algorithms cannot be combined in polynomial time},
  crossref = "cade96",
  pages    = {246-260},
  note     = "To appear in a special issue of " #ic,
}

@Article{Takahito2001jflp,
      author={Takahito Aoto},
      title={Solution to the Problem of {Z}antema on a Persistent
             Property of Term Rewriting Systems},
      journal={Journal of Functional and Logic Programming},
      volume={2001},
      number={11},
      month={December},
      year={2001}
}

@PhdThesis{Mellies:these,
  author =    {Melli{\`e}s, Paul-Andr\'e},
  title =     {Description Abstraite des Syst{\`e}mes de R{\'e}{\'e}criture},
  school =    {Universit{\'e} Paris VII},
  year =      1996,
  type =      {Th{\`e}se de doctorat},
  month =     {20 D\'ecembre}
}

@InProceedings{Oostrom97rta,
  author =       {Oostrom, Vincent van},
  title =        {Finite Family Developments},
  crossref = 	 "rta97",
  pages =        {308--322},
}


@InProceedings{comon01focs,
  author = "Hubert Comon and Guillem Godoy and Robert Nieuwenhuis",
  title = "The Confluence of Ground Term Rewrite Systems is Decidable
                 in Polynomial Time",
  crossref = "focs01",
  pages = "298--307"
}

@InProceedings{tiwari02lics,
  title = {Deciding Confluence of Certain Term Rewriting Systems in
              Polynomial Time},
  author = {Ashish Tiwari},
  pages  = {447--456},
  crossref = "lics02"
}

@InProceedings{korovin01icalp,
  title = "{K}nuth-{B}endix Constraint Solving Is {NP}-Complete",
  author = "Konstantin Korovin and Andrei Voronkov",
  crossref = "icalp01",
  pages = "979--992",
}

@InProceedings{korovin00lics,
  title = "A Decision Procedure for the Existential Theory of Term Algebras
            with the {K}nuth-{B}endix Ordering",
  author = "Konstantin Korovin and Andrei Voronkov",
  crossref = "lics00",
  pages = "291--302"
}

@InProceedings{korovin02unif,
  title = "The Decidability of the First-Order Theory of the {K}nuth-{B}endix
              orders in the case of unary signatures",
  author = "Konstantin Korovin and Andrei Voronkov",
  crossref = "unif02",
  pages = "45--46"
}

@InProceedings{korovin02fsttcs,
  title = "The decidability of the first-order theory of the
             {K}nuth-{B}endix orders in the case of unary signatures",
  author = "Konstantin Korovin and Andrei Voronkov",
  crossref = "fsttcs02",
  note = "A preliminary report of the result appeared in \cite{korovin02unif}"
}

@InProceedings{levy02rta,
  author = "Jordi Levy and Mateu Villaret",
  title = "Currying Second-Order Unification Problems",
  crossref = "rta02",
  pages = "326--339",
}

@InProceedings{plandowski99focs,
  author   = "Wojciech Plandowski",
  title    = "Satisfiability of Word Equations with Constants is in {PSPACE}",
  crossref = "focs99",
  pages    = "495-500",
}

@Article{Squier1987a,
  author       = "Craig Squier",
  title        = "Word Problems and a Homological Finiteness Condition
                 for Monoids",
  journal      = "J. of Pure and Applied Algebra",
  volume       = "49",
  year         = "1987",
  pages        = "201--217",
}

@INCOLLECTION{Simpson85a,
    AUTHOR = "S.G. Simpson",
    TITLE = "Nonprovability of certain combinatorial properties of
             finite trees",
    BOOKTITLE = "Harvey Friedman's research on the Foundation of
                   Mathematics",
    PUBLISHER = elsevier,
    PAGES = "87--117",
    YEAR = 1985,
    EDITOR = "L. A. Harrington"
    }

@ARTICLE{Kriz89,
    AUTHOR = "I. K\v{r}\'{\i}\v{z}",
    TITLE  = "Well-quasiordering finite trees with gap-condition.
              Proof of {H}arvey {F}riedman's conjecture",
    JOURNAL = "Ann. of Math.",
    VOLUME = 130,
    PAGES = "215--226",
    YEAR  = 1989
    }

@ARTICLE{Gordeev90,
    AUTHOR = "L. Gordeev",
    TITLE  = "Generalizations of the {K}ruskal-{F}riedman theorems",
    JOURNAL = jsl,
    VOLUME = 55,
    NUMBER = 1,
    PAGES = "157--181",
    YEAR  = 1990
    }

@INPROCEEDINGS{Mizuhito95,
    AUTHOR = "Ogawa, M.",
    TITLE = "Simple gap termination on term graph rewriting systems",
    BOOKTITLE = "Theory of Rewriting Systems and Its Application",
    YEAR = 1995,
    PAGES = "99--108",
    NOTE = "Research report 918, RIMS, Kyoto Univ, Kyoto.,
            also available at http://www.brl.ntt.co.jp/people/mizuhito"
    }

@InProceedings{geser03rta,
  author = "Alfons Geser",
  title = "Termination of String Rewriting Rules That Have One Pair
           of Overlaps",
  crossref = "rta03",
  pages = "410--423"
}

@Article{walukiewicz03jfp,
  author =	 {Daria Walukiewicz-Chrzaszcz},
  title =        {Termination of rewriting in the {C}alculus of
                 {C}onstructions},
  journal =	 {Journal of Functional Programming},
  year =         2003,
  volume =	 {13},
  number =	 {2},
  pages =        {339--414}
}

@Misc{blanqui03mscs,
  author =	 {Fr\'ed\'eric Blanqui},
  title =        {Definitions by rewriting in the {C}alculus of 
                 {C}onstructions},
  year =         2003,
  note =         {To appear in Mathematical Structures in Computer Science}
}

@Article{godoy04aaecc,
  author = "Guillem Godoy and Ashish Tiwari and Rakesh Verma",
  title =  "Characterizing Confluence by Rewrite Closure and Right Ground Term Rewrite Systems",
  journal = aaecc,
  volume = 15,
  number = 1,
  year = 2004,
  month = jun,
  pages = "13--36",
  url = "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0938-1279&volume=15&issue=1&spage=13",
}

@TechReport{scheffermann:pr309,
  author = "Kai Scheffermann",
  title = "A Countererexample to the Modularity of Unicity of Normal Forms
                 for Join Conditional Term Rewriting Systems",
  year = 2002,
  month = apr,
  institution = "Universit{\"a}t Hannover, Institut f{\"ur} Mathematik",
  type = "Preprint",
  number = "pr309",
  ps = "http://www-ifm.math.uni-hannover.de/preprints/pr309.ps",
  pdf = "http://www-ifm.math.uni-hannover.de/preprints/pr309.pdf",
  dvi = "http://www-ifm.math.uni-hannover.de/preprints/pr309.dvi",
}

@InProceedings{ohsaki01csl,
  author = "Hitoshi Ohsaki",
  title = "Beyond Regularity: Equational Tree Automata for Associative
            and Commutative Theories",
  crossref = "csl01",
  pages = "539-553"
}

@InProceedings{ohsaki02rta,
  author = "Hitoshi Ohsaki and Toshinori Takai",
  title = "Decidability and Closure Properties of Equational Tree Languages",
  pages = "114-128",
  crossref = "rta02",
}

@InProceedings{dalzilio-lugiez03rta,
  author = "Silvano Dal Zilio and Denis Lugiez",
  title = "{XML} Schema, Tree Logic and Sheaves Automata",
  pages = "246-263",
  crossref = "rta03"
}


@article{AG00,
  author        = "Thomas Arts and J{\"u}rgen Giesl",
  title         = "Termination of Term Rewriting Using Dependency
                   Pairs",
  journal       = tcs,
  volume        = 236,
  year          = 2000,
  pages         = "133--178"
}


@article{DP86,
  author        = "Nachum Dershowitz and David Plaisted",
  title         = "Equational Programming",
  journal       = mi,
  volume        = "11",
  pages         = "21--56",
  year          = "1986"
}

@article{DH95,
  author        = "Nachum Dershowitz and Charles Hoot",
  title         = "Natural Termination",
  journal       = tcs,
  volume        = "142",
  pages         = "170--207",
  year          = "1995"
}



@article{GA01,
  author        = "J{\"u}rgen Giesl and Thomas Arts",
  title         = "Verification of {E}rlang Processes by Dependency
                   Pairs",
  journal       = aaecc,
  volume        = "12",
  number        = "1,2",
  pages         = "39--72",
  year          = "2001"
}

@InProceedings{AProVE,
  author = 	 {J{\"u}rgen Giesl and R. Thiemann and P. Schneider-Kamp and
                  S. Falke},
  title = 	 {Automated Termination Proofs with {{\sf AProVE}}},
  pages =        {210--220},
  crossref =     "rta04",
}

@InProceedings{GM87,
  author = 	 {E. Giovanetti and C. Moiso},
  title = 	 {Notes on the Elimination of Conditions},
  booktitle = 	 {Proc.\ CTRS~'87},
  series = 	 {LNCS 308},
  pages =        {91--97},
  year =         {1987}
}



@PhdThesis{HootPhD,
  author = 	 {Charles Hoot},
  title = 	 {Termination of Non-Simple Rewrite Systems},
  school = 	 univill,
  year = 	 {1996}
}

@InProceedings{M96,
  author = 	 {M. Marchiori},
  title = 	 {Unravelings and Ultra-Properties},
  booktitle = 	 {Proc.\ ALP~'96},
  series = 	 {LNCS 1139},
  pages =        {107--121},
  year =         {1996}
}


@article{O01,
  author        = "Enno Ohlebusch",
  title         = "Termination of Logic Programs: Transformational Methods
                  Revisited",
  journal       = aaecc,
  volume        = "12",
  number        = "1,2",
  pages         = "73--116",
  year          = "2001"
}

@InProceedings{TALP,
  author =   {Enno Ohlebusch and Claus Claves and Claude March\'e},
  title =    {{\sf TALP}: A Tool for the Termination Analysis of Logic
                Programs},
  crossref=  "rta00",
  pages =    {270--273},
}

@phdthesis{Sivakumar89:uiuc,
     author = "G. Sivakumar",
     year = 1989,
     month = may,
     title = "Proofs and Computations in Conditional Equational Theories",
     school = csill # ", " # univill, 
     note = "Report R-89-1642",
     address = "Urbana, IL",
}

@ARTICLE{Bertrand-94,
  AUTHOR = {A. Bertrand},
  TITLE  = {Sur une conjecture {d'Yves} {M\'etivier}},
  JOURNAL = tcs,
  VOLUME = 123,
  NUMBER = 1,
  YEAR = 1994,
  PAGES = {21-30},
}

@Article{simonsen04ipl,
  author = "Jakob Grue Simonsen",
  title  = "On confluence and residuals in {C}auchy convergent
            transfinite rewriting",
  journal = ipl,
  volume  = 91,
  number  = 3,
  year    = 2004,
  month   = aug,
  pages   = "141--146",
  url     = "http://linkinghub.elsevier.com/retrieve/pii/S0020019004001103",
}
  

@Article{CourcelleKnapik02tcs,
  author     = "Bruno Courcelle and Teodor Knapik",
  title      = "The evaluation of first-order substitution is monadic
                   second-order compatible",
  journal    = tcs,
  volume     = 281,
  number     = "1--2",
  pages      = "177--206",
  year       = 2002,
  month      = jun
}

@Article{BauderonCourcelle87mst,
  author    = "Michel Bauderon and Bruno Courcelle",
  title     = "Graph Expressions and Graph Rewritings",
  journal   =  mst,
  volume    =  20,
  number    = "2--3",
  pages     = "83-127",
  year      = 1987
}

@InProceedings{Dershowitz05OpenClosed,
  author    = "Nachum Dershowitz",
  title     = "{O}pen. {C}losed. {O}pen",
  crossref  = "rta05",
  url       = "http://www.cs.tau.ac.il/\home{nachumd}/papers/OpenClosed.pdf"
}

@Article{marche96jsc,
  AUTHOR = {Claude March{\'e}},
  TITLE = {Normalized Rewriting: an alternative to Rewriting
                  modulo a Set of Equations},
  JOURNAL = jsc,
  YEAR = 1996,
  month = mar,
  VOLUME = 21,
  NUMBER = 3,
  PAGES = {253--288},
  url = "ftp://ftp.lri.fr/LRI/articles/marche/jsc96.ps.gz"
}

@InProceedings{zhang05cade,
  author  = "Ting Zhang and Henny Sipma and Zohar Manna",
  title   = "The Decidability of the First-order Theory of {K}nuth-{B}endix
                 Order",
  crossref = "cade05",
  url      = "http://theory.stanford.edu/\home{sipma}/papers/cade05.html",
  pages    = "131--148",
}

@Misc{HofbauerWaldmann05termination,
  author = "Dieter Hofbauer and Johannes Waldmann",
  title  = "Termination of $\{aa \rightarrow bc, bb \rightarrow ac,
               cc \rightarrow ab\}$",
  howpublished = "Preprint",
  year = 2005,
  url = "http://www.theory.informatik.uni-kassel.de/\home{dieter}/research/papers/Z086.ps.gz",
}

@TechReport{Stoevring:RS-05-35,
    author =     "Kristian St{\o}vring",
    title =      "Extending the Extensional Lambda Calculus with
                            Surjective Pairing is Conservative",
    institution =  "DAIMI, Department of Computer Science, University of
                            Aarhus",
    year =       2005,
    month =      nov,
    type =       "Research Report",
    number =     "BRICS RS-05-35",
    address =    "Aarhus, Denmark",
    url =        "http://www.brics.dk/RS/05/35/"
  }

@Article{Stoevring:LMCS-2006,
    author =     "Kristian St{\o}vring",
    title =      "Extending the Extensional Lambda Calculus with
    Surjective Pairing is Conservative",
    journal = "Logical Methods in Computer Science",
    volume = 2,
    number = {2:1},
    pages = {1-14},
    year = 2006,
url = "http://www.lmcs-online.org/ojs/viewarticle.php?id=140&layout=abstract",
}

@Article{buechi86,
author	= {J. Richard B{\"u}chi and Steven Senger},
title	= "Coding in the Existential Theory of Concatenation",
journal	= "Archiv math. Logik",
volume	= 26,
year	= "1986",
pages	= "101--106",
}

@Article{durnev95siberia,
  author   = "Valery G. Durnev",
  title    = "Undecidability of the Positive $\forall\exists^3$-Theory
                  of a Free Semigroup",
  journal  = "Siberian Mathematical Journal",
  year     = 1995,
  month    = sep#"--"#oct,
  volume   = 36,
  number   = 5,
  pages    = "917--929",
  note     = "English translation of \cite{durnev95sibirskiy}"
}

@Article{durnev95sibirskiy,
  author   = "Valery G. Durnev",
  title    = "Undecidability of the Positive $\forall\exists^3$-Theory
                  of a Free Semigroup",
  journal  = "Sibirski\v{\i}{} Matematicheski\v{\i}{} Zhurnal",
  year     = 1995,
  month    = sep,
  volume   = 36,
  number   = 5,
  pages    = "1067--1080",
  note     = "English translation as \cite{durnev95siberia}"
}

@Article{karhumaeki00jacm,
author = {Juhani Karhum\"aki and Filippo Mignosi and Wojciech Plandowski},
title = "The Expressibility of Languages and Relations by Word Equations",
journal = jacm,
year = 2000,
month = may,
pages = "483--505",
volume = 47,
number = 5
}

@Inproceedings{ohsaki05lpar,
author = "Hitoshi Ohsaki and Jean-Marc Talbot and Sophie Tison and Yves Roos",
title = "Monotone {AC}-Tree Automata",
crossref = "lpar05",
pages = "337--351"
}

@inproceedings{stirling06icalp,
  author    = {Colin Stirling},
  title     = {A Game-Theoretic Approach to Deciding Higher-Order Matching.},
  crossref  = "icalp06-2",
  pages     = {348-359},
}

@article{moser:aaecc2009,
  author = {Georg Moser},
  title = {The {H}ydra Battle and {C}ichon's Principle},
  journal = aaecc,
  year = {2009},
  note = {\texttt{doi:10.1007/s00200-009-0094-4}},
  volume = 20,
  number = 2,
  pages = {133-158},
  url = "http://www.springerlink.com/content/100499/?Content+Status=Accepted"
}



 
@string{lics={Symposium on Logic in Computer Science}}

@Proceedings{aaai93,
  booktitle = 	 "Proceedings of the eleventh national conference on
		  artificial intelligence",
  title = 	 "Proceedings of the eleventh national conference on
		  artificial intelligence",
  year = 	 1993,
  number =	 11,
  address =	 "Washington, DC"
}

@Proceedings{acl86,
  booktitle	= "24th Annual Meeting of the Association for Computational
			Lingustics",
  title	        = "24th Annual Meeting of the Association for Computational
			Lingustics",
  key           = "ACL86",
  address	= "New York, NY",
  year		= 1986
}

@Proceedings{acl87,
  booktitle	= "25th Annual Meeting of the Association for Computational
                	Lingustics",
  title	        = "25th Annual Meeting of the Association for Computational
                	Lingustics",
  key           = "ACL87",
  year		= 1987,
}

@Proceedings{alp92,
  booktitle	= "3th International Conference on Algebraic and
			Logic Programming",
  title	        = "3th International Conference on Algebraic and
			Logic Programming",
  editor	= "H\'el\`ene Kirchner and Giorgio Levi",
  month		= sep,
  year		= 1992,
  publisher	= springer,
  series	= lncs,
  volume 	= 632,
  address	= "Volterra, Italy",
}

@Proceedings{alp94,
  booktitle	= "4th International Conference on Algebraic and
			Logic Programming",
  title	= "4th International Conference on Algebraic and
			Logic Programming",
  editor	= "Giorgio Levi and Mario Rodr{\'\i}guez-Artalejo",
  month		= sep,
  year		= 1994,
  publisher	= springer,
  series	= lncs,
  volume 	= 850,
  address	= "Madrid, Spain",
}

@Proceedings{alp96,
  booktitle     = "5th International Conference on Algebraic and
                        Logic Programming",
  title     = "5th International Conference on Algebraic and
                        Logic Programming",
  editor        = "Michael Hanus and Mario Rodr{\'\i}guez-Artalejo",
  month         = sep,
  year          = 1996,
  publisher     = springer,
  series        = lncs,
  volume        = 1139,
  address       = "Aachen, Germany",
}

@Proceedings{alp97,
  booktitle	= "6th International Conference on Algebraic and
			 Logic Programming",
  title	= "6th International Conference on Algebraic and
			 Logic Programming",
  year		= 1997,
  publisher	= springer,
  series	= lncs,
  volume	= 1298,
}

@Proceedings{plilp95,
  booktitle     = "7th International Symposium on Programming Languages:
                   Implementations, Logics and Programs",
  title     = "7th International Symposium on Programming Languages:
                   Implementations, Logics and Programs", 
  editor        = "S. Doaitse Swierstra and M. Hermenegildo",
  month         = sep,
  year          = 1995,
  publisher     = springer,
  series        = lncs,
  volume        = 982,
  address       = "Utrecht, The Netherlands",
}


@Proceedings{caap91,
  booktitle	= "Colloquium on Trees in Algebra and Programming",
  title	= "Colloquium on Trees in Algebra and Programming",
  year		= 1991, 
  series	= lncs,
  publisher	= springer,
}

@Proceedings{caap94,
  booktitle	= "Colloquium on Trees in Algebra and Programming",
  title	= "Colloquium on Trees in Algebra and Programming",
  editor	= "Sophie Tison",
  year		= 1994,
  address	= "Edinburgh, Scotland", 
  series	= lncs,
  volume        = 787,
  publisher	= springer,
}

@proceedings{cade80,
  booktitle	= "5th~International Conference on Automated Deduction",
  title	= "5th~International Conference on Automated Deduction",
  address	= "Les Arcs, France",
  editor	= "W.~Bibel and R.~Kowalski",
  series	= lncs,
  volume 	= 87,
  publisher	= springer,
  year		= 1980
}

@proceedings{cade82,
  booktitle	= "6th International Conference on Automated Deduction",
  title	= "6th International Conference on Automated Deduction",
  address	= "New York, USA",
  editor	= "D. W. Loveland",
  series	= lncs,
  volume 	= 138,
  publisher	= springer,
  year		= 1982
}

@proceedings{cade84,
  booktitle	= "7th International Conference on Automated Deduction",
  title	= "7th International Conference on Automated Deduction",
  address	= "Napa, California, USA",
  editor	= "R. E. Shostak",
  series	= lncs,
  volume 	= 170,
  publisher	= springer,
  year		= 1984
}

@Proceedings{cade86,
  booktitle	= "8th International Conference on Automated Deduction",
  title	= "8th International Conference on Automated Deduction",
  address	= "Oxford, England",
  editor	= {J\"rg Siekmann},
  series	= lncs,
  volume 	= 230,
  publisher	= springer,
  year		= 1986,
}

@Proceedings{cade88,
  booktitle = 	 "9th International Conference on Automated Deduction",
  title = 	 "9th International Conference on Automated Deduction",
  year = 	 1988,
  month		= may,
  editor =	 "Lusk and Overbeek",
  volume =	 310,
  series =	 lncs,
  publisher =	 springer,
  address =	 "Argonne, Illinois"
}

@Proceedings{cade90,
  booktitle	= "10th International Conference on Automated Deduction",
  title	= "10th International Conference on Automated Deduction",
  address	= "Kaiserslautern, Germany",
  editor	= "M. E. Stickel",
  year		= 1990,
  month		= jul,
  publisher	= springer,
  series	= LNAI,
  volume 	= 449,
}

@proceedings{cade92,
  booktitle	= "11th International Conference on Automated Deduction",
  title	        = "11th International Conference on Automated Deduction",
  address	= "Saratoga Springs, NY",
  editor	= "Deepak Kapur",
  year		= 1992,
  month		= jun,
  publisher	= springer,
  series	= lncs,
  volume =    "607"
}

@proceedings{cade94,
  booktitle	= "12th International Conference on Automated Deduction",
  title	        = "12th International Conference on Automated Deduction",
  editor	= "A. Bundy",
  address	= "Nancy, France",
  publisher     = springer,
  series        = lncs,
  year		= 1994,
  volume	= 814,
}

@proceedings{cade96,
  booktitle	= "13th International Conference on Automated Deduction",
  title	        = "13th International Conference on Automated Deduction",
  address	= "New Brunswick, NJ",
  editor	= "M. A. McRobbie and J. K. Slaney",
  year		= 1996,
  month		= jul #"/"# aug,
  publisher	= springer,
  series	= lncs,
}

@proceedings{cade97,
  booktitle	= "14th International Conference on Automated Deduction",
  title	        = "14th International Conference on Automated Deduction",
  address	= "Townsville, Australia",
  editor	= "William McClune",
  year		= 1997,
  month		= jul,
  publisher	= springer,
  series	= lnai,
  volume	= 1249
}

@Proceedings{cade99,
  booktitle     = "16th International Conference on Automated Deduction",
  title         = "16th International Conference on Automated Deduction",
  address       = "Trento, Italy",
  month         = jul,
  year          = 1999,
  editor        = "Harald Ganzinger",
  publisher     = springer,
  series        = lnai,
  volume        = 1632
}

@Proceedings{cade05,
  booktitle     = "20th International Conference on Automated Deduction",
  title         = "20th International Conference on Automated Deduction",
  editor        = "Robert Nieuwenhuis",
  address       = "Tallinn, Estonia",
  month         = jul,
  year          = 2005,
  publisher     = springer,
  series        = lncs,
  volume        = 3632,
}

@Proceedings{ccl94,
  booktitle	= "First International Conference on Constraints in Computational Logics",
  title	        = "First International Conference on Constraints in Computational Logics",
  editor	= "Jean-Pierre Jouannaud",
  address	= "M{\"u}nchen, Germany",
  month		= sep,
  year		= 1994,
  series	= lncs,
  volume	= 845,
  publisher	= springer,
}

@Proceedings{cp95,
  booktitle =  "Principles and Practice of Constraint Programming",
  title =      "Principles and Practice of Constraint Programming",
  year = 	 1995,
  editor =	 "Ugo Montanari and Francesca Rossi",
  publisher	= springer,
  address =	 "Cassis, France",
  month =	 sep,
  series	= lncs,
  volume	= 976
}

@Proceedings{cp97,
  booktitle =  "Principles and Practice of Constraint Programming",
  title =  "Principles and Practice of Constraint Programming",
  year = 	 1997,
  editor =	 "Gert Smolka",
  publisher	= springer,
  address =	 "Linz, Austria",
  month =	 oct,
  series	= lncs,
  volume	= 1330
}

@Proceedings{csl91,
  booktitle	= "Computer Science Logic",
  editor	= {E. B{\"o}rger and G. J{\"a}ger and H. Kleine B{\"u}ning and
			M. M. Richter},
  year		= 1991,
  month		= oct,
  address	= "Berne, Switzerland",
  series	= lncs,
  publisher	= springer,
  volume = 626
}

@Proceedings{csl94,
  booktitle	= "Proceedings of the 8th Workshop on Computer Science Logic",
  year		= 1994,
  month		= sep,
  editor	= "Leszek Pacholski and Jerzy Tiuryn",
  address	= "Kazimierz, Poland",
  publisher	= springer,
  series	= lncs,
  volume   = 933
}

@Proceedings{csl97,
  booktitle	= "Proceedings of the Conference on Computer Science Logic",
  editor =       {M. Nielsen and Wolfgang Thomas},
  yea 		= 1997,
  publisher	= springer,
  series	= lncs,
  volume	= 1414,
  address	= "Aarhus, Denmark",
  year		= 1997,
  month		= aug,
}

@Proceedings{csl01,
  booktitle = "15th International Workshop on Computer Science Logic",
  editor    = "Laurent Fribourg",
  publisher = springer,
  series    = lncs,
  volume    = 2142,
  year      = 2001,
  month     = sep,
  address   = "Paris, France",
}

@Proceedings{ctrs91,
  booktitle    = "Proceedings of the Second International Workshop on
                        Conditional and Typed Rewriting Systems",
  title        = "Proceedings of the Second International Workshop on
                        Conditional and Typed Rewriting Systems",
  address      = "Montreal, Canada",
  editor       = "M. Okada",
  volume       = 516,
  series       = lncs,
  publisher    = springer,
  year         = 1991,
}

@Proceedings{ctrs92,
  booktitle 	=   "Proceedings of the Third International Workshop on
                 	Conditional Rewriting Systems",
  title 	=   "Proceedings of the Third International Workshop on
                 	Conditional Rewriting Systems",
  editor 	= {Micha\"el Rusinowitch, M. and R\'emy, J. L.},
  month		= jan,
  year		= 1993,
  publisher	= springer,
  series	= lncs,
  volume	= 656,
  address	= {Pont-\`a-Mousson, France},
}

@Proceedings{ctrs94,
  booktitle =   "Proceedings of the Fourth International Workshop on
                 	Conditional Rewriting Systems",
  title =   "Proceedings of the Fourth International Workshop on
                 	Conditional Rewriting Systems",
  address = 	"Jerusalem, Israel",
  month	=	jul,
  year =        1994,
  publisher =   springer,
  editor =      "Nachum Dershowitz and N. Lindenstrauss"
}

@Proceedings{focs78,
  booktitle	= "19th Annual Symposion on Foundations of Computer Science",
  title	        = "19th Annual Symposion on Foundations of Computer Science",
  key           = "FOCS78",
  year		= 1978,
  month		= oct,
  address	= "Ann Arbor, Michigan",
  publisher	= ieee,
}

@Proceedings{focs93,
  booktitle	= "Proc. 34th Symposium on Foundations of Computer Science",
  title	        = "Proc. 34th Symposium on Foundations of Computer Science",
  key           = "FOCS93",
  publisher	= ieee,
  year		= 1993,
  month		= nov,
  address	= "Palo Alto, CA",
}

@Proceedings{focs94,
  booktitle	= "Proceedings of the $35^{th}$ Symposium on
                        Foundations of Computer Science",
  title	        = "Proceedings of the $35^{th}$ Symposium on
                        Foundations of Computer Science",
  key           = "FOCS94",
  year		= 1994,
}

@Proceedings{focs98,
  title	       = "Proceedings of the $39^{th}$ Symposium on
                        Foundations of Computer Science",
  booktitle	= "Proceedings of the $39^{th}$ Symposium on
                        Foundations of Computer Science",
  key           = "FOCS98",
  year		= 1998,
}

@Proceedings{focs99,
  title	        = "Proceedings of the $40^{th}$ Symposium on
                        Foundations of Computer Science",
  booktitle	= "Proceedings of the $40^{th}$ Symposium on
                        Foundations of Computer Science",
  key           = "FOCS99",
  year		= 1999,
  month         = oct,
  address       = "New York, NY, USA",
  publisher     = ieee
}


@Proceedings{focs01,
  booktitle  = "Proceedings of the 42nd Annual IEEE Symposium on Foundations
                       of Computer Science (FOCS)",
  title = "Proceedings of the 42nd Annual IEEE Symposium on Foundations
                       of Computer Science (FOCS)",
  key = "FOCS01",
  address = "Las Vegas, Nevada, USA",
  year = 2001,
}

@Proceedings{fplca85,
  booktitle	= "IFIP International Conference on Functional Programming
                        Languages and Computer Architecture",
  title	        = "IFIP International Conference on Functional Programming
                        Languages and Computer Architecture",
  year		= 1985,
  editor	= "Jean-Pierre Jouannaud",
  series	= lncs,
  publisher	= springer,
  volume = 201
}

@Proceedings{fsttcs90,
  booktitle	= "Foundations of Software Technology and Theoretical Computer
               		 Science",
  title	        = "Foundations of Software Technology and Theoretical Computer
               		 Science",
  address	= "Bangalore, India",
  editor	= "K. V. Nori and C. E. Veni Madhavan",
  series	= lncs,
  volume = "472",
  publisher	= springer,
  year		= 1990,
}

@Proceedings{fsttcs92,
  booktitle	= "Foundations of Software Technology and Theoretical Computer
               		 Science",
  address	= "New Delhi, India",
  editor	= "R. Shyamasundar",
  series	= lncs,
  volume = "652",
  month = dec,
  publisher	= springer,
  year		= 1992,
}

@Proceedings{fsttcs02,
  booktitle   = "Foundations of Software Technology and Theoretical Computer Science",
  title   = "Foundations of Software Technology and Theoretical Computer Science",
  address     = "Kanpur, India",
  publisher   = springer,
  series      = lncs,
  month       = dec,
  year        = 2002,
  note        = "T o appear"
}

@proceedings{gwai85,
  booktitle	= "9th German Wokshop on Artificial Intelligence",
  title	= "9th German Wokshop on Artificial Intelligence",
  address	= "Dassel/Solling",
  editor	= "Herbert Stoyan",
  series	= "Informatik Fachberichte vol. 118",
  publisher	= springer,
  year		= 1985
}

@proceedings{gwai86,
  booktitle	= "10th German Wokshop on Artificial Intelligence",
  title	= "10th German Wokshop on Artificial Intelligence",
  address	= "Ottenstein/Nieder{\"o}sterreich",
  editor	= "W. Bibel and R. Kowalski",
  series	= "Informatik Fachberichte vol. 124",
  publisher	= springer,
  year		= 1986
}

@Proceedings{icalp87,
  booktitle	= "14th International Colloquium on
                        Automata, Languages and Programming",
  title	= "14th International Colloquium on
                        Automata, Languages and Programming",
  editor	= "Thomas Ottmann",
  year		= 1987,
  month		= jul,
  address	= "Karlsruhe, Germany",
  publisher	= springer,
  series	= lncs,
  volume =    "267",
}

@proceedings{icalp89,
  booktitle	= "16th International Colloquium on
                        Automata, Languages and Programming",
  title	= "16th International Colloquium on
                        Automata, Languages and Programming",
  address	= "Stresa, Italy",
  year		= 1989,
  month		= jul,
  series = lncs,
  publisher = springer,
  volume = 372,
}

@proceedings{icalp90,
  booktitle	= "17th International Colloquium on
                	Automata, Languages and Programming",
  title	= "17th International Colloquium on
                	Automata, Languages and Programming",
  address	= "Warwick, England",
  editor	= "M. S. Paterson",
  series	= lncs,
  volume =    "443",
  publisher	= springer,
  year		= 1990
}

@proceedings{icalp91,
  booktitle	= "18th International Colloquium on
			Automata, Languages and Programming",
  title	= "18th International Colloquium on
			Automata, Languages and Programming",
  address	= "Madrid, Spain",
  editor	= "Javier Leach Albert and Burkhard Monien and M. Rodriguez Artalejo",
  publisher	= springer,
  series	= lncs,
  volume =    "510",
  year		= 1991
}

@proceedings{icalp92,
  booktitle	= "19th International Colloquium on
                	Automata, Languages and Programming",
  title	= "19th International Colloquium on
                	Automata, Languages and Programming",
  address	= "Wien, Austria",
  editor	= "Werner Kuich",
  publisher	= springer,
  series	= lncs,
  volume        = 623,
  year		= 1992,
  month		= jul,
}

@proceedings{icalp93,
  booktitle	= "20th International Colloquium on
                        Automata, Languages and Programming",
  title	= "20th International Colloquium on
                        Automata, Languages and Programming",
  address	= "Lund, Sweden",
  editor	= "Andrzej Lingas and Rolf Karlsson and Svante Carlsson",
  publisher	= springer,
  series	= lncs,
  volume =    "700",
  year		= 1993,
  month		= jul,
}

@proceedings{icalp94,
  booktitle	= "21th International Colloquium on
                        Automata, Languages and Programming",
  title	= "21th International Colloquium on
                        Automata, Languages and Programming",
  address	= "Jerusalem, Israel",
  editor	= "Serge Abiteboul and Eli Shamir",
  publisher	= springer,
  series	= lncs,
  volume =    "820",
  year		= 1994,
  month		= jul,
}

@Proceedings{icalp01,
  editor    = {Fernando Orejas and Paul G. Spirakis and Jan van Leeuwen},
  title     = "28th International Colloquium on Automata, Languages and Programming",
  booktitle = "28th International Colloquium on Automata, Languages and Programming",
  publisher = springer,
  series    = lncs,
  volume    = {2076},
  year      = {2001},
  isbn      = {3-540-42287-0},
  month     = jul,
  address   = "Crete, Greece",
}

@proceedings{icalp06-2,
  editor    = {Michele Bugliesi and
               Bart Preneel and
               Vladimiro Sassone and
               Ingo Wegener},
  title     = {Automata, Languages and Programming, 33rd International
               Colloquium, Part II},
  booktitle = {ICALP (2)},
  publisher = springer,
  series    = lncs,
  volume    = {4052},
  year      = {2006},
  month     = jul,
  address   = "Venice, Italy",
  isbn      = {3-540-35907-9},
}

@Proceedings{iclp87,
  booktitle	= "Proceedings of the Fourth International Conference on
			Logic Programming",
  title	= "Proceedings of the Fourth International Conference on
			Logic Programming",
  editor	= "Jean-Louis Lassez",
  year		= 1987,
  month		= may,
  publisher	= mitpress,
}

@Proceedings{iclp90,
  booktitle	= "Proceedings of the 7th International Conference on
			Logic Programming",
  title	= "Proceedings of the 7th International Conference on
			Logic Programming",
  year		= 1990,
  month		= jun,
  editor	= "D.H.D. Warren and P. Szeredi",
  publisher	= mitpress,
}

@Proceedings{iclp91,
  booktitle	= "Proceedings of the 8th International Conference on
                	Logic Programming",
  title	= "Proceedings of the 8th International Conference on
                	Logic Programming",
  year		= 1991,
  month		= jun,
  address	= "Paris, France",
  editor	= "Koichi Furukawa",
  publisher	= mitpress,
}

@Proceedings{iclp93,
  editor =       "David S. Warren",
  series =       "Logic Programming",
  booktitle =    "Proceedings of the Tenth International Conference
                       on Logic Programming",
  title =        "Proceedings of the Tenth International Conference
                       on Logic Programming",
  year =         1993,
  publisher =    mitpress,
  address =      "Budapest, Hungary",
  month =        jun
}

@Proceedings{iclp94,
  booktitle	= "Proceedings of the Eleventh International Conference on
                	Logic Programming",
  title	= "Proceedings of the Eleventh International Conference on
                	Logic Programming",
  year		= 1994,
  monyth	= jun,
  address	= "Santa Margherita Ligure, Italy",
  editor	= "Pascal van Hentenryck",
  publisher	= mitpress,
}

@Proceedings{ijcai91,
  booktitle	= "International Joint Conference on Artificial Intelligence",
  title	= "International Joint Conference on Artificial Intelligence",
  year		= 1991
}

@Proceedings{ijcai93,
  booktitle	= "13th International Joint Conference on Artificial
			Intelligence",
  title	= "13th International Joint Conference on Artificial
			Intelligence",
  month		= aug,
  year		= 1993,
  address	= "Chamb\'ery, France",
  publisher	= "Morgan Kaufmann"
}

@Proceedings{islp91,
  booktitle	= {Proceedings of the 1991 International Symposium
			on Logic Programming},
  title	= {Proceedings of the 1991 International Symposium
			on Logic Programming}, 
  year		= 1991,
  editor	= "Saraswat, Vijay and Ueda, Kazunori",
  publisher	= mitpress,
  address	= {San Diego, USA},     
}

@Proceedings{islp93,
  booktitle	= "Proceedings of the 1993 International Symposium
			on Logic Programming",
  title	= "Proceedings of the 1993 International Symposium
			on Logic Programming",
  editor	= "Dale Miller",
  year		= 1993,
  month		= oct,
  address	= "Vancouver, Canada",
  publisher	= mitpress,
}

@Proceedings{iwnmsa93,
  booktitle = 	 {Proceedings of the international workshop on new models
			of software architecture},
  title = 	 {Proceedings of the international workshop on new models
			of software architecture},
  year = 	 1993,
  address =	 {Japan},
  month =	 {November}
}

@Proceedings{jicslp92,
  booktitle	= "Proceedings of the Joint International Conference and
               		 Symposium on Logic Programming",
  title	= "Proceedings of the Joint International Conference and
               		 Symposium on Logic Programming",
  editor	= "Apt, Krzysztof",
  year		= 1992,
  month		= nov,
  publisher	= mitpress,
  address	= "Washington, USA"
}

@Proceedings{lics86,
  booktitle	= "First " # lics,
  title	        = "First " # lics,
  month		= jun,
  year		= 1986,
  address	= "Cambridge, MA",
  publisher	= ieee,
}

@Proceedings{lics87,
  booktitle	= "Second " # lics,
  title	        = "Second " # lics,
  year		= 1987,
  organization	= ieee,
}

@Proceedings{lics88,
  booktitle	= "Third " # lics,
  title	        = "Third " # lics,
  editor	= "Yuri Gurevich",
  year		= 1988,
  month		= jul,
  address	= "Edinburgh, Scotland",
  organization	= ieee,
}


@Proceedings{lics89,
  booktitle	= "Fourth " # lics,
  title	        = "Fourth " # lics,
  year		= 1989,
  organization	= ieee,
}

@Proceedings{lics90,
  booktitle	= "Fifth " # lics,
  title	        = "Fifth " # lics,
  editor	= "John C. Mitchell",
  year		= 1990,
  month		= jun,
  address	= "Philadelphia, PA",
  organization	= ieee,
}

@Proceedings{lics91,
  booktitle	= "Sixth " # lics,
  title	        = "Sixth " # lics,
  editor	= "Gilles Kahn",
  year		= 1991,
  month		= jul,
  address	= "Amsterdam, The Netherlands",
  organization	= ieee,
}

@Proceedings{lics92,
  booktitle	= "Seventh " # lics,
  title	        = "Seventh " # lics,
  editor	= "Andre Scedrov",
  year		= 1992,
  month		= jun,
  address	= "Santa Cruz, CA",
  organization	= ieee,
}

@Proceedings{lics93,
  booktitle	= "Eigth " # lics,
  title	        = "Eigth " # lics,
  editor	= "Moshe Y. Vardi",
  year		= 1993,
  month		= jun,
  address	= "Montreal, Canada",
  organization	= ieee,
}

@Proceedings{lics94,
  booktitle	= "Ninth " # lics,
  title	        = "Ninth " # lics,
  editor	= "Samson Abramsky",
  year		= 1994,
  month		= jul,
  address	= "Paris, France",
  organization	= ieee,
}

@Proceedings{lics95,
  booktitle	= "Tenth " # lics,
  title	        = "Tenth " # lics,
  editor	= "Dexter Kozen",
  year		= 1995,
  month		= jun,
  address	= "San Diego, CA",
  organization	= ieee,
}

@Proceedings{lics96,
  booktitle	= "Eleventh " # lics,
  title	        = "Eleventh " # lics,
  editor	= "Edmund C. Clarke",
  year		= 1996,
  month		= jul,
  address	= "New Brunswick, NJ",
  organization	= ieee,
}

@Proceedings{lics97,
  booktitle     = "Twelfth " # lics,
  title         = "Twelfth " # lics,
  editor	= "Glynn Winskel",
  year          = 1997,
  month         = jun,
  address       = "Warsaw, Poland",
  organization  = ieee,
}

@Proceedings{lics98,
  booktitle	= "Thirteenth IEEE Annual Symposium on Logic in Computer Science",
  title	        = "Thirteenth IEEE Annual Symposium on Logic in Computer Science",
  editor	= "Vaughan Pratt",
  year		= 1998,
  month		= jun,
  address	= "Indianapolis, IN",
  organization	= ieee,
}

@Proceedings{lics99,
  booktitle     = "Fourteenth IEEE Annual Symposium on Logic in Computer Science",
  title     = "Fourteenth IEEE Annual Symposium on Logic in Computer Science",
  year		= 1999,
  month		= jul,
  address	= "Trento, Italy",
  organization  = ieee,
}

@Proceedings{lics00,
  booktitle = "15th Annual {IEEE} Symposium on Logic in Computer Science",
  title = "15th Annual {IEEE} Symposium on Logic in Computer Science",
  year      = 2000,
  month     = jun,
  address   = "Santa Barbara, CA, USA",
  organization = ieee,
}

@Proceedings{lics02,
  booktitle = "{{IEEE Symposium on Logic in Computer Science, LICS 2002}}",
  title = "{{IEEE Symposium on Logic in Computer Science, LICS 2002}}",
  editor = {Gordon Plotkin},
  publisher = ieee,
  month = jul,
  year = 2002,
  address = "Copenhagen, Denmark"
}

@Proceedings{lpar92,
  booktitle	= "International Conference on Logic Programming and
			Automated Reasoning",
  editor	= "A. Voronkov",
  year		= 1992,
  month		= jul,
  address	= "St. Petersburg, Russia",
  publisher	= springer,
  series	= LNAI,
  volume = 624,
}

@Proceedings{lpar93,
  booktitle	= "4th International Conference on Logic Programming and
			Automated Reasoning",
  editor	= "Andrei Voronkov",
  year		= 1993,
  month		= jul,
  address	= "St. Petersburg, Russia",
  publisher	= springer,
  series	= LNAI,
  volume = 698,
}

@Proceedings{lpar05,
  booktitle = "12th International Conference on Logic Programming and Automated Reasoning",
  editor = "Geoff Sutcliffe and Andrei Voronkov",
  year = 2005,
  month = dec,
  series = LNAI,
  publisher = springer,
  volume = 3835,
  address = "Montego Bay, Jamaica",
}

@Proceedings{mfcs80,
  booktitle	= "Mathematical Foundations of Computer Science",
  editor        = "Piotr Dembinski",
  title	        = "Mathematical Foundations of Computer Science",
  year		= 1980,
  month		= sep,
  address	= "Rydzyna, Poland"
}

@Proceedings{mfcs84,
  booktitle	= "Mathematical Foundations of Computer Science",
  title	        = "Mathematical Foundations of Computer Science",
  editor	= "M. P. Chytil and V. Koubek",
  month		= sep,
  year		= 1984,
  address	= "Praha, Czechoslovakia",
  publisher	= springer,
  series	= lncs,
  volume = 175,
}

@Proceedings{mfcs91,
  booktitle	= "Mathematical Foundations of Computer Science",
  title	        = "Mathematical Foundations of Computer Science",
  editor	= "Andrzej Tarlecki",
  year		= 1991,
  month		= sep,
  address	= "Kazimierz Dolny, Poland",
  publisher	= springer,
  series	= LNAI,
  volume        = 520,
}

@Proceedings{mfcs92,
  booktitle     = "Mathematical Foundations of Computer Science",
  title         = "Mathematical Foundations of Computer Science",
  editor        = "Ivan M. Havel and V{\'a}clav Koubek",
  address       = "Prague, Czechoslovakia",
  year		= 1992,
  month         = aug,
  publisher	= springer,
  series        = lncs,
  volume        = 629
}

@Proceedings{mfcs93,
  booktitle	= "Mathematical Foundations of Computer Science",
  title	        = "Mathematical Foundations of Computer Science",
  editor	= "Andrzej M. Borzyszkowski and Stefan Soko{\l}owski",
  year		= 1993,
  month		= "30 August--3 September",
  address	= "Gda\'nsk, Poland",
  publisher	= springer,
  series	= lncs,
  isbn		= "3-540-57182-5",
  volume = 711,
}

@Proceedings{mfcs98,
  editor =       {Lubos Brim and Jozef Gruska and Jir\'{\i} Zlatuska},
  booktitle =    "Mathematical Foundations of Computer Science",
  title =        "Mathematical Foundations of Computer Science",
  address =      "Brno, Czech Republic",
  series =       lncs,
  volume =       1450,
  publisher =    springer,
  year =         1998,
  month =        aug,
}

@Proceedings{pods91,
  booktitle   = "Tenth {ACM} Symposium on the Principles of Database Systems",
  title	      = "Tenth {ACM} Symposium on the Principles of Database Systems",
  key         = "PODS91",
  month	      = may,
  year	      = 1991,
  address     = "Denver, CO",
  publisher   = acm,
}

@proceedings{popl75,
  booktitle	= "Proceedings of 2nd {ACM} Conference on Principles
             		of Programming Languages",
  title	        = "Proceedings of 2nd {ACM} Conference on Principles
             		of Programming Languages",
  key           = "POPL75",
  year		= 1975,
  address	= "Palo Alto, CA",
  publisher	= acm,
}

@Proceedings{popl80,
  booktitle	= "Proccedings of the Seventh Annual {ACM} Symposion on
			Principles of Programming Languages",
  title	        = "Proccedings of the Seventh Annual {ACM} Symposion on
			Principles of Programming Languages",
  key           = "POPL80",
  year		= 1980,
  month		= jan,
  address	= "Las Vegas, Nevada",
  publisher	= acm,
}

@proceedings{popl85,
  booktitle	= "Proceedings of 12th {ACM} Conference on Principles
             		of Programming Languages",
  title	        = "Proceedings of 12th {ACM} Conference on Principles
             		of Programming Languages",
  key           = "POPL85",
  editor	= "B. Reid",
  year		= 1985,
  publisher	= acm,
}

@proceedings{popl87,
  booktitle	= "Proceedings of the 14th {ACM} Conference on Principles
             		of Programming Languages",
  title	        = "Proceedings of the 14th {ACM} Conference on Principles
             		of Programming Languages",
  key           = "POPL87",
  address	= "Munich, Germany",
  month		= jan,
  year		= 1987,
  publisher	= acm,
}

@proceedings{popl90,
  booktitle	= "Proceedings of the 17th {ACM} Conference on Principles
             		of Programming Languages",
  title	        = "Proceedings of the 17th {ACM} Conference on Principles
             		of Programming Languages",
  key           = "POPL90",
  address	= "San Francisco, CA",
  month		= jan,
  year		= 1990,
  publisher     = acm,
}

@proceedings{popl91,
  booktitle	= "Proceedings of the 18th Symposium on Principles of
			Programming Languages",
  title	        = "Proceedings of the 18th Symposium on Principles of
			Programming Languages",
  key           = "POPL91",
  address	= "Orlando, FL",
  month		= jan,
  year		= 1991,
  publisher	= acm,
}

@proceedings{popl92,
  booktitle	= "Conference Record of the 19th Symposium on Principles of
			Programming Languages",
  title	        = "Conference Record of the 19th Symposium on Principles of
			Programming Languages",
  key           = "POPL92",
  address	= "Albuquerque, NM",
  year		= 1992,
  publisher	= acm,
}

@Proceedings{popl94,
  booktitle	= "Conference Record of the 21st Symposium on Principles of
                	Programming Languages",
  title	        = "Conference Record of the 21st Symposium on Principles of
                	Programming Languages",
  key           = "POPL94",
  year		= 1994,
  address	= "Portland, Oregon",
  publisher	= acm,
}

@Proceedings{popl97,
  booktitle = 	 {Conference Record of the 21st Symposium on Principles of
                	Programming Languages},
  title = 	 {Conference Record of the 21st Symposium on Principles of
                	Programming Languages},
  key =          "POPL97",
  year = 	 1997,
  publisher =	 acm,
  month =        jan,
  address =	 {Paris, France}
}

@Proceedings{ppcp94,
  booktitle	= "Principles and Practice of Constraint Programming",
  title	        = "Principles and Practice of Constraint Programming",
  key           = "PPCP94",
  year		= 1994,
  address	= "Orcas Island, Washington, USA",
}


@proceedings{rta87,
  booktitle	= "Rewriting Techniques and Applications",
  title	        = "Rewriting Techniques and Applications",
  editor	= "Pierre Lescanne",
  series	= lncs,
  publisher	= springer,
  year		= 1987,
  month		= may,
  address	= "Bordeaux, France",
  volume	= 256
}

@Proceedings{rta89,
  booktitle	= "Rewriting Techniques and Applications",
  title	        = "Rewriting Techniques and Applications",
  editor	= "Nachum Dershowitz",
  series	= lncs,
  publisher	= springer,
  year		= 1989,
  month		= apr,
  address	= "Chapel Hill, NC, USA",
  volume	= 355
}

@Proceedings{rta91,
  booktitle	= "4th International Conference on Rewriting Techniques and Applications",
  title	        = "4th International Conference on Rewriting Techniques and Applications",
  editor	= "Ronald. V. Book",
  year		= 1991,
  month		= apr,
  address	= "Como, Italy",
  publisher	= springer,
  series	= lncs,
  volume	= 488,
}

@Proceedings{rta93,
  title	=       "5th International Conference on Rewriting Techniques and Applications",
  booktitle	= "5th International Conference on Rewriting Techniques and Applications",
  editor	= "Claude Kirchner",
  publisher	= springer,
  year		= 1993,
  month		= jun,
  address	= "Montreal, Canada",
  series	= lncs,
  volume 	= 690,
}

@Proceedings{rta95,
  booktitle	= "6th International Conference on Rewriting Techniques and Applications",
  title	= "6th International Conference on Rewriting Techniques and Applications",
  editor	= "Jieh Hsiang",
  publisher	= springer,
  year		= 1995,
  month		= apr,
  address	= "Kaiserslautern, Germany",
  series	= lncs,
  volume	= 914
}

@Proceedings{rta96,
  booktitle	= "7th International Conference on Rewriting Techniques and Applications",
  title	= "7th International Conference on Rewriting Techniques and Applications",
  editor	= "Harald Ganzinger",
  publisher	= springer,
  year		= 1996,
  month		= jul,
  address	= "New Brunswick, NJ, USA",
  series	= lncs,
  volume	= 1103,
}

@Proceedings{rta97,
  booktitle	= "8th International Conference on Rewriting Techniques and Applications",
  title	= "8th International Conference on Rewriting Techniques and Applications",
  editor	= "Hubert Comon",
  publisher	= springer,
  year		= 1997,
  month		= jun,
  address	= "Barcelona, Spain",
  series	= lncs,
  volume	= 1232,
}

@Proceedings{rta98,
  booktitle	= "9th International Conference on Rewriting Techniques and Applications",
  title	= "9th International Conference on Rewriting Techniques and Applications",
  editor	= "Tobias Nipkow",
  publisher	= springer,
  year		= 1998,
  month		= apr,
  address	= "Tsukuba, Japan",
  series	= lncs,
  volume	= 1379,
}

@Proceedings{rta99,
  booktitle	= "10th International Conference on Rewriting Techniques and Applications",
  title	= "10th International Conference on Rewriting Techniques and Applications",
  editor	= "Paliath Narendran and Michael Rusinowitch",
  publisher	= springer,
  month		= jul,
  year		= 1999,
  address	= "Trento, Italy",
  series	= lncs,
  volume	= 1631,
}
  
@Proceedings{rta00,
  booktitle     = "Rewriting Techniques and Applications",
  title     = "Rewriting Techniques and Applications",
  editor        = "Leo Bachmair",
  publisher     = springer,
  series        = lncs,
  volume        = 1833,
  month         = jul,
  year          = 2000,
  address       = "Norwich, UK"
}

@Proceedings{rta01,
  booktitle     = "Rewriting Techniques and Applications",
  title     = "Rewriting Techniques and Applications",
  editor        = "Aart Middeldorp",
  publisher     = springer,
  series        = lncs,
  volume        = 2051,
  month         = may,
  year          = 2001,
  address       = "Utrecht, The Netherlands",
}

@Proceedings{rta02,
  booktitle     = "Rewriting Techniques and Applications",
  title     = "Rewriting Techniques and Applications",
  editor        = "Sophie Tison",
  publisher     = springer,
  series        = lncs,
  volume        = 2378,
  month         = jul,
  year          = 2002,
  address       = "Copenhagen, Denmark",
}

@Proceedings{rta03,
  title         = "14th International Conference on Rewriting Techniques",
  booktitle     = "14th International Conference on Rewriting Techniques",
  editor        = "Robert Nieuwenhuis",
  publisher     = springer,
  year          = 2003,
  month         = jun,
  address       = "Valencia, Spain",
  series        = LNCS,
  volume        = 2706
}

@Proceedings{rta04,
  title         = "15th International Conference on Rewriting Techniques",
  booktitle     = "15th International Conference on Rewriting Techniques",
  editor        = "Vincent van Oostrom",
  publisher     = springer,
  year          = 2004,
  month         = jun,
  address       = "Aachen, Germany",
  series        = LNCS,
  volume        = 3091
}

@Proceedings{rta05,
  title         = "16th International Conference on Rewriting Techniques",
  booktitle     = "16th International Conference on Rewriting Techniques",
  editor        = {J\"urgen Giesl},
  publisher     = springer,
  series        = lncs,
  volume        = 3467,
  address       = "Nara, Japan",
  month         = apr,
  year          = 2005
}

@Proceedings{srt97,
  booktitle = 	 {Proceedings of the Conference on Symbolic Rewriting
		  	Techniques},
  title = 	 {Proceedings of the Conference on Symbolic Rewriting
		  	Techniques},
  year = 	 1997,
  editor =	 {Manuel Bronstein and Volker Weispfenning},
  publisher =	 BIRK,
  address =	 {Monte Verita, Switzerland}
}

@Proceedings{stacs91,
  booktitle = "Eighth Symposium on Theoretical Aspects of Computer Science",
  title     = "Eighth Symposium on Theoretical Aspects of Computer Science",
  editor    = "Christian Choffrut and Matthias Jantzen",
  month	    = feb,
  year	    = 1991,
  address   = "Hamburg, Germany",
  publisher = springer,
  series    = lncs,
  volume    = 480,
}

@Proceedings{stacs93,
  booktitle=	"Symposium on Theoretical Aspects of Computer Science",
  title =	"Symposium on Theoretical Aspects of Computer Science",
  editor =      "Patrice Enjalbert and Alain Finkel and Klaus W. Wagner",
  series = 	lncs,
  publisher = 	springer,
  volume =      665,
  year	=	1993,
  month =       feb,
  address = 	{W{\"u}rzburg, Germany},
}

@Proceedings{tacs91,
  booktitle	= "Theoretical Aspects of Computer Software",
  title	        = "Theoretical Aspects of Computer Software",
  editor	= "T. Ito and A. R. Meyer",
  series	= lncs,
  volume        = "526",
  year		= 1991,
  month		= sep,
  publisher	= springer
}

@Proceedings{tapsoft-caap85,
  booktitle	= "Proceedings of the International Joint Conference on
			Theory and Practice of Software Development --
                        Colloquium on Trees in Algebra and Programming",
  title	        = "Proceedings of the International Joint Conference on
			Theory and Practice of Software Development --
                        Colloquium on Trees in Algebra and Programming",
  editor        = "Hartmut Ehrig and Christiane Floyd and Maurice Nivat
                        and James W. Thatcher",
  year		= 1985,
  month         = march,
  publisher	= springer,
  series	= lncs,
  volume        = 185
}


@Proceedings{tapsoft87-2,
  booktitle	= "Proceedings of the International Joint Conference on
			Theory and Practice of Software Development",
  title	= "Proceedings of the International Joint Conference on
			Theory and Practice of Software Development",
  year		= 1987,
  publisher	= springer,
  volume	= 2,
  address	= "Pisa, Italy",
  series	= lncs,
  volume =    "250",
}


@Proceedings{tapsoft89-1,
  booktitle	= "Proceedings of the International Joint Conference
		  	on Theory and Practice of Software Development",
  volume	= "1 - Advanced Seminar on Foundations of Innovative Software
			Development {I} and Colloquium on Trees in Algebra
			and Programming",
  editor	= "J. D\'{\i}az and  F. Orejas",
  year		= 1989,
  month		= mar,
  address	= "Barcelona, Spain",
  publisher	= springer,
  series	= lncs,
  volume =    "351"
}

@Proceedings{tapsoft93,
  booktitle	= "4th International Joint Conference on
			Theory and Practice of Software Development",
  title	= "4th International Joint Conference on
			Theory and Practice of Software Development",
  editor	= "M. C. Gaudel and J.-P. Jouannaud",
  year		= 1993,
  month		= apr,
  address	= "Orsay, France",
  publisher	= springer,
  series	= lncs,
  volume = 668,
}

@Proceedings{tapsoft97,
  booktitle	= "Theory and Practice of Software Development",
  title	        = "Theory and Practice of Software Development",
  editor	= "Michel Bidoit and Max Dauchet",
  year		= 1997,
  month		= apr,
  address	= "Lille, France", 
  series	= lncs,
  volume        = "1214",
  publisher	= springer,
}

@Proceedings{tlca93,
  booktitle = 	 "International Conference of Typed Lambda Calculi and
			Applications",
  title = 	 "International Conference of Typed Lambda Calculi and
			Applications",
  key =          "TLCA93",
  year = 	 "1993"
}

@Proceedings{tlca95,
  booktitle   = "Typed Lambda Calculi and Applications",
  title       = "Typed Lambda Calculi and Applications",
  year	      = 1995,
}

@Proceedings{unif02,
  editor = "Christophe Ringeissen and Cesare Tinelli and Ralf Treinen
            and Rakesh M. Verma",
  booktitle = "Proceedings of the 16th International Workshop on Unification ({UNIF 2002)}",
  title = "Proceedings of the 16th International Workshop on Unification ({UNIF 2002)}",
  series = "Technical Report 02-05, " #deptcsiowa,
  month = jul,
  year = 2002,
  address = "Copenhagen, Denmark",
}

@Proceedings{wadt92,
  booktitle = 	 {Proceedings 10th workshop on abstract data types (1992).},
  title = 	 {Proceedings 10th workshop on abstract data types (1992).},
  year = 	 1994,
  publisher =	 springer,
  address =	 {Caldes de Malevella, Spain},
  month =	 oct,
}

@Book{lothaire:words02,
  editor      = "M. Lothaire",
  booktitle   = "Algebraic Combinatorics on Words",
  title       = "Algebraic Combinatorics on Words",
  publisher   = cambridgepress,
  year        = 2002,
  isbn        = "0 521 81220 8",
}

@Proceedings{lacl98,
  title =        "Logical Aspects of Computational Linguistics",
  year =         2001,
  pages =        "106-125",
  address =      "Grenoble, France",
}