@string{conf:TPHOLs = "Theorem Proving in Higher Order Logics, TPHOLs"}
@string{conf:RTA    = "Rewriting Techniques and Applications, RTA"}
@string{conf:LPAR   = "Logic for Programming, Artificial Intelligence, and Reasoning, LPAR"}
@string{ai    = "Acta Informatica"}
@string{jar   = "Journal of Automated Reasoning"}
@string{lncs = "LNCS"}
@string{lipics = "Leibniz International Proceedings in Informatics"}


@article{WPO,
  author    = {Akihisa Yamada and
               Keiichirou Kusakari and
               Toshiki Sakabe},
  title     = {{A unified ordering for termination proving}},
  journal   = {Sci. Comput. Program.},
  volume    = {111},
  pages     = {110--134},
  year      = {2015},
  doi       = {10.1016/j.scico.2014.07.009},
  timestamp = {Thu, 08 Jun 2017 08:59:10 +0200},
  biburl    = {https://dblp.org/rec/journals/scp/0002KS15.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{WPO-PPDP,
  author    = {Akihisa Yamada and
               Keiichirou Kusakari and
               Toshiki Sakabe},
  editor    = {Ricardo Pe{\~{n}}a and
               Tom Schrijvers},
  title     = {Unifying the {K}nuth-{B}endix, recursive path and polynomial orders},
  booktitle = {15th International Symposium on Principles and Practice of Declarative
               Programming, {PPDP} '13, Madrid, Spain, September 16-18, 2013},
  pages     = {181--192},
  publisher = {{ACM}},
  year      = {2013},
  doi       = {10.1145/2505879.2505885},
  timestamp = {Tue, 06 Nov 2018 16:57:25 +0100},
  biburl    = {https://dblp.org/rec/conf/ppdp/YamadaKS13.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}


@inproceedings{WPO_form_paper,
  author    = {Ren{\'{e}} Thiemann and
               Jonas Sch{\"{o}}pf and
               Christian Sternagel and
               Akihisa Yamada},
  editor    = {Zena M. Ariola},
  title     = {Certifying the Weighted Path Order (Invited Talk)},
  booktitle = {5th International Conference on Formal Structures for Computation
               and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual
               Conference)},
  series    = {LIPIcs},
  volume    = {167},
  pages     = {4:1--4:20},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2020},
  url       = {https://doi.org/10.4230/LIPIcs.FSCD.2020.4},
  doi       = {10.4230/LIPIcs.FSCD.2020.4},
  timestamp = {Tue, 30 Jun 2020 11:42:59 +0200},
  biburl    = {https://dblp.org/rec/conf/fscd/ThiemannSS020.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}
}
@unpublished{LPO,
  author        = "S. Kamin and J.~J. L{\'{e}}vy",
  title         = "Two Generalizations of the Recursive Path Ordering",
  note          = "Unpublished Manuscript, University of Illinois, IL,
                   USA",
  year          = "1980"
}

@article{WPO_AFP,
  author  = {Christian Sternagel and René Thiemann and Akihisa Yamada},
  title   = {A Formalization of Weighted Path Orders and Recursive Path Orders},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2021},
  note    = {\url{https://isa-afp.org/entries/Weighted_Path_Order.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
