2005-journal.bib

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

@comment{{Command line: /usr/bin/bib2bib -q -oc 2005-journal.cite -ob 2005-journal.bib -c 'year = 2005 and topics : "team" and $type="article"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}

@article{krstic-conchon-05,
  author = {Sava Krsti{\'c} and Sylvain Conchon},
  title = {Canonization for disjoint unions of theories},
  journal = {Information and Computation},
  volume = {199},
  month = {May},
  year = {2005},
  pages = {87--106},
  topics = {team},
  number = {1-2},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {JIC}
}

@article{contejean05jar,
  author = {\'Evelyne Contejean and Claude March{\'e} and Ana Paula Tom{\'a}s and Xavier Urbain},
  title = {Mechanically proving termination using polynomial
   interpretations},
  journal = {Journal of Automated Reasoning},
  volume = {34},
  number = {4},
  pages = {325--363},
  year = 2005,
  type_publi = {irevcomlec},
  topics = {team},
  doi = {10.1007/s10817-005-9022-x},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {JAR},
  abstract = {http://www.lri.fr/~contejea/publis/2005jar/abstract.html}
}

@article{lucas05ipl,
  topics = {team},
  author = {Salvador Lucas and Claude March\'e and Jos\'e Meseguer},
  title = {Operational Termination of Conditional Term Rewriting Systems},
  journal = {Information Processing Letters},
  publisher = {Elsevier North-Holland, Inc.},
  volume = 95,
  pages = {446--453},
  year = 2005,
  type_publi = {irevcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {IPL},
  x-international-audience = {yes},
  x-language = {en},
  abstract = {We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs}
}