% rewriting.bib
% Aaron Stump, 5/3/00
%
% This file contains some references to works about rewriting.

@inproceedings{KB70,
title={{Simple Word Problems in Universal Algebras}},
pages={263--297},
author="D. Knuth and P. Bendix",
booktitle={{Computational Problems in Abstract Algebra}},
editor="J. Leech",
year=1970,
publisher="Pergamon Press"
}

@article{D87,
author= "N. Dershowitz",
title={{Termination of Rewriting}},
journal="Journal of Symbolic Computation",
volume="3",
number="1 and 2",
pages="69-116",
year="1987"}

@book{BN98,
author = "F. Baader and T. Nipkow",
title = {{Term Rewriting and All That}},
publisher = "Cambridge University Press",
year="1998"}

@book{B91,
author = "L. Bachmair",
title = {{Canonical Equational Proofs}},
series = "Progress in Theoretical Computer Science",
publisher = "Birkh{\"a}user",
year = "1991"}


@ARTICLE{cirstea01d,
  AUTHOR = {Cirstea, H. and Kirchner, C.},
  TITLE = {{The Rewriting Calculus - Part I}},
  JOURNAL = {Logic Journal of the Interest Group in Pure and Applied
		  Logics},
  MONTH = {May},
  PAGES = {363-399},
  VOLUME = {9},
  YEAR = {2001},
  NOTE = {Also available as Technical Report A01-R-203, LORIA, Nancy
		  (France)}
}


@ARTICLE{cirstea01e,
  AUTHOR = {Cirstea, H. and Kirchner, C.},
  TITLE = {{The Rewriting Calculus - Part II}},
  JOURNAL = {Logic Journal of the Interest Group in Pure and Applied
		  Logics},
  MONTH = {May},
  PAGES = {401-434},
  VOLUME = {9},
  YEAR = {2001},
  NOTE = {Also available as Technical Report A01-R-204, LORIA, Nancy
		  (France)}
}

@Article{CDELMMQspecprog_2001,
  author =       {Manuel Clavel and Francisco Dur{\'a}n and Steven Eker and
                  Patrick Lincoln and Narciso Mart{\'\i}-Oliet and Jos{\'e}
                  Meseguer and Jos{\'e} F. Quesada},
  title =        {{Maude}: Specification and Programming in Rewriting Logic},
  journal =      {Theoretical Computer Science},
  volume = 285,
  number = 2,
  year =         2002
}

@INPROCEEDINGS{ppts-popl2003,
  AUTHOR = {G. Barthe and H. Cirstea and C. Kirchner and L. Liquori},
  TITLE = {Pure Patterns Type Systems},
  BOOKTITLE = {{ Principles of Programming Languages}},
  YEAR = 2003,
  PUBLISHER = {ACM},
  PS = {data/ppts-popl2003.ps.gz},
}

@inproceedings{Vis01.rule,
  author    = {E. Visser},
  title     = {Scoped Dynamic Rewrite Rules},
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {59/4},
  publisher = {Elsevier Science Publishers},
  editor    = {Mark van den Brand and Rakesh Verma},
  year      = {2001},
  booktitle = {Rule Based Programming (RULE'01)},
  urlpdf    = {http://www.cs.uu.nl/people/visser/ftp/Vis01-rule.pdf}
}

@INPROCEEDINGS{rewritingStrategiesWRS2003,
  AUTHOR = {H. Cirstea and C. Kirchner and L. Liquori and B. Wack},
  TITLE = {Rewrite Strategies in the Rewriting Calculus},
  BOOKTITLE = {{Proceedings of the Third International Workshop on Reduction Strategies 
                  in Rewriting and Programming }},
  YEAR = 2003,
  MONTH = JUN,
  PUBLISHER = {Electronic Notes in Theoretical Computer Science},
  EDITOR = {B. Gramlich and S. Lucas},
  ADDRESS = {Valencia, Spain}
}

@INPROCEEDINGS{CirsteaKirchnerLiquoriMatchingPower-RTA2001,
  AUTHOR = {H. Cirstea and C. Kirchner and L. Liquori},
  TITLE = {{M}atching {P}ower},
  YEAR = {2001},
  BOOKTITLE = {Proceedings of the 12th International Conference on Rewriting Techniques and Applications},
  ADDRESS = {Utrecht (The Netherlands)},
  EDITOR = {A. Middeldorp},
  PUBLISHER = {Springer-Verlag},
  SERIES = "LNCS"
}

@inproceedings{clavel00reflection,
    author = {Manuel Clavel and Jos{'e} Meseguer},
    title = {{Reflection and Strategies in Rewriting Logic}},
    booktitle = {Electronic Notes in Theoretical Computer Science},
    volume = {4},
    publisher = {Elsevier Science Publishers},
    editor = {J. Meseguer},
    year = {2000}
}

@InCollection{CDEMprovingtools_2000,
  author = 	 {M. Clavel and F. Dur{\'a}n and S. Eker and J. Meseguer},
  title = 	 {{Building Equational Proving Tools by Reflection in 
                  Rewriting Logic}},
  booktitle = 	 {Cafe: An Industrial-Strength Algebraic Formal Method},
  publisher =    {Elsevier},
  year = 	 {2000},
}

@article{mes92,
author = "J. Meseguer",
title={{Conditional Rewriting Logic as a Unified Model of Concurrency}},
journal={Theoretical Computer Science},
volume=96,
number=1,
year=1992,
pages={73-155}}

@unpublished{color05,
title={{CoLoR: a Coq Library on Rewriting and Termination}},
note={Available at http://color.loria.fr},
year=2005}

@inproceedings{giesl+04,
author = "J. Giesl and R. Thiemann and P. Schneider-Kamp and S. Falke",
title={{Automated Termination Proofs with AProVE}},
booktitle="the 15th International Conference on Rewriting Techniques and Applications",
year=2004,
publisher="Springer",
pages="210--220",
editor="V. van Oostrom"}

@inproceedings{arts96,
author="T. Arts",
title={{Termination by absence of infinite chains of dependency pairs}},
editor="H. Kirchner",
booktitle="International Colloquium on Trees in Algebra and Programming",
year=1996}

@InCollection{BDP89,
  author =       {L. Bachmair and N. Dershowitz and D.A. Plaisted},
  title =        {{Completion Without Failure}},
  booktitle =    {Resolution of Equations in Algebraic Structures},
  year =         1989,
  publisher =    {Academic Press},
  volume =       {2, Rewriting Techniques},
  pages =        "1--30"
}

@incollection{Zantema03,
author="H. Zantema",
editor="TERESE",
chapter=6,
title="Termination",
booktitle="Term Rewriting Systems",
pages="181--259",
publisher="Cambridge University Press",
year=2003}

@incollection{klop+03,
author="J. Klop and R. de Vrijer",
editor="TERESE",
chapter=3,
title={{Examples of TRSs and Special Rewriting Formats}},
booktitle="Term Rewriting Systems",
publisher="Cambridge University Press",
year=2003}

@article{giesl+02,
 author = {J. Giesl and T. Arts and E. Ohlebusch},
 title = {{Modular Termination Proofs for Rewriting Using Dependency Pairs}},
 journal = {Journal of Symbolic Computation},
 volume = {34},
 number = {1},
 year = {2002},
 pages = {21--58},
 publisher = {Academic Press, Inc.}
 }

@inproceedings{SK94,
  author = {A. Sattler-Klein},
  title = {{About Changing the Ordering During Knuth-Bendix Completion}},
  year = {1994},
  booktitle = {Symposium on Theoretical Aspects of Computer Science},
  volume="775",
  pages="176-186",
  editor = {E. W. Mayr, P. Enjalbert and K. W. Wagner},
  publisher = {Springer},
  series = "LNCS"
}

@article{H81,
author = {G. Huet},
title = {{A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm}},
journal = {Journal of Computer and System Science},
volume = "23",
number = "1",
year = "1981",
pages = "11-21"
}

@Incollection{DershowitzPlaisted:HandbookAR:rewriting:2001,
  title = {Rewriting},
  author = {N. Dershowitz and D.A. Plaisted},
  chapter = 9,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {535-610}}

@book{TeReSe,
  title= {Term Rewriting Systems},
  editor={TeReSe}, 
  publisher={Cambridge University Press},
  year=2003,
  volume=55,
  series={Cambridge Tracts in Theoretical Computer Science}
}

@article{ nieuwenhuis93simple,
    author = "Robert Nieuwenhuis",
    title = "Simple {LPO} Constraint Solving Methods",
    journal = "Information Processing Letters",
    volume = "47",
    number = "2",
    pages = "65-69",
    year = "1993",
    url = "citeseer.ist.psu.edu/nieuwenhuis93simple.html" }


@misc{ rta-summary-complete,
  author = "Nachum Dershowitz and Ralf Treinen",
  title = {{The RTA list of open problems}},
  url = "citeseer.ist.psu.edu/700125.html",
  howpublished = "\url{http://www.lsv.ens-cachan.fr/rtaloop/}" }



@INPROCEEDINGS{Dershowitz05OpenClosed,
  AUTHOR = {Nachum Dershowitz},
  TITLE = {{O}pen. {C}losed. {O}pen},
  URL = {http://www.cs.tau.ac.il/\home{nachumd}/papers/OpenClosed.pdf},
  CROSSREF = "rta05"
}

@Proceedings{rta05,
  title         = "16th International Conference on Rewriting Techniques",
  booktitle     = "16th International Conference on Rewriting Techniques",
  editor        = {J\"urgen Giesl},
  publisher     = {Springer-Verlag},
  series        = {Lecture Notes in Computer Science},
  volume        = 3467,
  address       = "Nara, Japan",
  month         = apr,
  year          = 2005
}

@ARTICLE{ComonTreinen93:lri,
  AUTHOR = {Hubert Comon and Ralf Treinen},
  TITLE = {The First-Order Theory of Lexicographic Path Orderings is
                Undecidable},
  JOURNAL = {Theoretical Computer Science},
  VOLUME = 176,
  NUMBER = {1--2},
  MONTH = APR,
  YEAR = 1997,
  PAGES = {67--87}
}

@Incollection{NieuwenhuisRubio:HandbookAR:paramodulation:2001,
  title = {Paramodulation-Based Theorem Proving},
  author = {R. Nieuwenhuis and A. Rubio},
  chapter = 7,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {371-443}}

@incollection{ dershowitz90rewrite,
    author = "Nachum Dershowitz and Jean-Pierre Jouannaud",
    title = "Rewrite Systems",
    booktitle = "Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B)",
    pages = "243--320",
    year = "1990",
    url = "citeseer.ist.psu.edu/dershowitz90rewrite.html" }

@inproceedings{ dershowitz91open,
    author = "Nachum Dershowitz and Jean-Pierre Jouannaud and Jan Willem Klop",
    title = "Open Problems in Rewriting",
    booktitle = "Proceedings of the Fourth International Conference on Rewriting Techniques and Applications (Como, Italy)",
    volume = "488",
    month = "April",
    publisher = "Springer-Verlag",
    address = "Berlin",
    editor = "R. Book",
    pages = "445--456",
    year = "1991",
    url = "citeseer.ist.psu.edu/article/dershowitz91open.html" }

@article{BachmairTiwariVigneron03:JAR,
	TITLE = {Abstract congruence closure},
	AUTHOR = {Leo Bachmair and Ashish Tiwari and Laurent Vigneron},
	JOURNAL = {J. of Automated Reasoning},
	PAGES = {129--168},
	PUBLISHER = {Kluwer Academic Publishers},
	VOLUME = 31,
	NUMBER = 2,
	YEAR = 2003,
}

@ARTICLE{1958PNAS...44.1061B,
   author = {{Boone}, W.~W.},
    title = "{The Word Problem}",
  journal = {Proceedings of the National Academy of Science},
     year = 1958,
    month = oct,
   volume = 44,
    pages = {1061-1065},
   adsurl = {http://adsabs.harvard.edu/cgi-bin/nph-bib_query?bibcode=1958PNAS...44.1061B&db_key=GEN},
  adsnote = {Provided by the Smithsonian/NASA Astrophysics Data System}
}

@article{ kapur95overview,
  author = 	 {D. Kapur and H. Zhang},
  title = 	 {{An overview of Rewrite Rule Laboratory (RRL)}},
  journal = 	 {J. Computer and Mathematics with Applications},
  year = 	 1995,
  volume =	 29,
  number =	 2,
  pages =	 {91-114},
  url = {citeseer.ist.psu.edu/kapur95overview.html} }

@MISC{cime3,
  AUTHOR = {Evelyne Contejean and Claude March{\'e} and 
                  Xavier Urbain},
  TITLE = {{CiME3}},
  NOTE = {Available at
                  \url{http://cime.lri.fr/}},
  YEAR = 2004,
  URL = {http://cime.lri.fr/},
  TOPICS = {team,lri}
}


@inproceedings{ detlefs85,
    author = "David Detlefs and Randy Forgaard.",
    title = "A Procedure for Automatically Proving the Termination of a Set of Rewrite Rules",
    booktitle = "Proceedings of the First International Conference on Rewriting Techniques and Applications (University of Dijon, France)",
    volume = "202",
    month = "May",
    publisher = "Springer-Verlag",
    address = "Berlin",
    editor = "Jean-Pierre Jouannaud",
    pages = {255-270},
    year = "1985"}

@inproceedings{ marche98termination,
    author = "Claude March\'e and Xavier Urbain",
    title = "Termination of Associative-Commutative Rewriting by Dependency Pairs",
    booktitle = "{RTA}",
    pages = "241--255",
    year = "1998",
    url = "citeseer.ist.psu.edu/marche98termination.html" }


@STRING{alp2	= "Proceedings 2nd International Conference on Algebraic and 
		   Logic Programming, {Nancy (France)}"}

@INPROCEEDINGS{lescanneALP90,
	AUTHOR = {Lescanne, P.},
	TITLE = {Implementation of Completion by Transition Rules +
		Control: {{\sc ORME}}},
	BOOKTITLE = alp2,
	YEAR = 1990,
	EDITOR = {Kirchner, H{\'e}l{\`e}ne and Wechler, W.},
	VOLUME = 463,
	PAGES = {262-269},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science}
}

@STRING{cade10	= "Proceedings 10th International Conference on Automated 
		   Deduction, Kaiserslautern (Germany)"}

@INPROCEEDINGS{lescanneORME,
	AUTHOR = {Lescanne, P.},
	TITLE = {{{\sc ORME}}, an Implementation of Completion Procedures as Sets 
		 of Transitions Rules},
	BOOKTITLE = cade10,
	YEAR = {1990},
	EDITOR = {Stickel, M.},
	PAGES = {661-662},
	PUBLISHER = {Springer-Verlag}
}

@inproceedings{clavel00reflection,
    author = {Manuel Clavel and Jos{'e} Meseguer},
    title = {Reflection and strategies in rewriting logic},
    booktitle = {Electronic Notes in Theoretical Computer Science},
    volume = {4},
    publisher = {Elsevier Science Publishers},
    editor = {J. Meseguer},
    year = {2000}
}

@inproceedings{ clavel98metalevel,
  author = "M. Clavel and F. Dur\'an and S. Eker and P. Lincoln and N. Mart\'i-Oliet  and J. Meseguer",
  title = {{Metalevel Computation in Maude}},
  booktitle = "Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications",
  series = "Electronic Notes in Theoretical Computer Science",
  publisher = "Elsevier",
  year = "1998"}


@INPROCEEDINGS{cirstea+03,
   author = {H. Cirstea and C. Kirchner and L. Liquori 
and B. Wack},
   title = {{Rewrite Strategies in the Rewriting Calculus}},
   booktitle = {{Proceedings of the Third International Workshop on
Reduction Strategies
                   in Rewriting and Programming }},
   year = 2003,
   publisher = {ENTCS},
   editor = {B. Gramlich and S. Lucas}}

@inproceedings{Sattler-Klein91,
  author    = {Andrea Sattler-Klein},
  title     = {Divergence Phenomena during Completion.},
  booktitle = {Rewriting Techniques and Applications, 4th International
               Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings},
  editor    = {Ronald V. Book},
  year      = {1991},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {488},
  pages     = {374-385},
}

@inproceedings{Kop06a,
  author    = {Adam Koprowski},
  title     = {{TPA}: Termination Proved Automatically.},
  booktitle = {Term Rewriting and Applications, 17th International Conference,
               RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings},
  year      = {2006},
  pages     = {257-266},
  ee        = {http://dx.doi.org/10.1007/11805618_19},
  editor    = {Frank Pfenning},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4098},
  year      = {2006},
  isbn      = {3-540-36834-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Socher-Ambrosius91,
  author    = {Rolf Socher-Ambrosius},
  title     = {Boolean Algebra Admits No Convergent Term Rewriting System},
  booktitle     = {Proceedings of the Fourth International Conference on Rewriting Techniques and Applications (RTA '91)},
  year      = {1991},
  pages     = {264-274},
  address   = "Como, Italy"
}

@inproceedings{hsiang83,
 author = {Jieh Hsiang and Nachum Dershowitz},
 title = {Rewrite Methods for Clausal and Non-Clausal Theorem Proving},
 booktitle = {Proceedings of the 10th Colloquium on Automata, Languages and Programming},
 year = {1983},
 pages = {331--346},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }
