@inproceedings{RPO_NPC,
  author    = {Ren{\'{e}} Thiemann and
               Guillaume Allais and
               Julian Nagele},
  editor    = {Ashish Tiwari},
  title     = {On the Formalization of Termination Techniques based on Multiset Orderings},
  booktitle = {23rd International Conference on Rewriting Techniques and Applications
               (RTA'12) , {RTA} 2012, May 28 - June 2, 2012, Nagoya, Japan},
  series    = {LIPIcs},
  volume    = {15},
  pages     = {339--354},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2012},
  url       = {https://doi.org/10.4230/LIPIcs.RTA.2012.339},
  doi       = {10.4230/LIPIcs.RTA.2012.339},
  timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
  biburl    = {https://dblp.org/rec/conf/rta/ThiemannAN12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{RPO,
  author    = {Nachum Dershowitz},
  title     = {Termination of Rewriting},
  journal   = {J. Symb. Comput.},
  volume    = {3},
  number    = {1/2},
  pages     = {69--116},
  year      = {1987},
  doi       = {10.1016/S0747-7171(87)80022-6},
  timestamp = {Wed, 14 Nov 2018 10:27:09 +0100},
  biburl    = {https://dblp.org/rec/journals/jsc/Dershowitz87.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{RPO_NP,
  author    = {Michael Codish and
               J{\"{u}}rgen Giesl and
               Peter Schneider{-}Kamp and
               Ren{\'{e}} Thiemann},
  title     = {{SAT} Solving for Termination Proofs with Recursive Path Orders and
               Dependency Pairs},
  journal   = {J. Autom. Reason.},
  volume    = {49},
  number    = {1},
  pages     = {53--93},
  year      = {2012},
  url       = {https://doi.org/10.1007/s10817-010-9211-0},
  doi       = {10.1007/s10817-010-9211-0},
  timestamp = {Wed, 02 Sep 2020 13:29:58 +0200},
  biburl    = {https://dblp.org/rec/journals/jar/CodishGST12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jsat/EenS06,
  author    = {Niklas E{\'{e}}n and
               Niklas S{\"{o}}rensson},
  title     = {Translating Pseudo-Boolean Constraints into {SAT}},
  journal   = {J. Satisf. Boolean Model. Comput.},
  volume    = {2},
  number    = {1-4},
  pages     = {1--26},
  year      = {2006},
  url       = {https://doi.org/10.3233/sat190014},
  doi       = {10.3233/sat190014},
  timestamp = {Mon, 17 Aug 2020 18:32:39 +0200},
  biburl    = {https://dblp.org/rec/journals/jsat/EenS06.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
