Halting Problem of One Binary Horn Clause is Undecidable

Philippe Devienne, Patrick Lebègue, Jean-Christophe Routier. Halting Problem of One Binary Horn Clause is Undecidable. In Patrice Enjalbert, Alain Finkel, Klaus W. Wagner, editors, STACS 93, 10th Annual Symposium on Theoretical Aspects of Computer Science, Würzburg, Germany, February 25-27, 1993, Proceedings. Volume 665 of Lecture Notes in Computer Science, pages 48-57, Springer, 1993.

@inproceedings{DevienneLR93,
  title = {Halting Problem of One Binary Horn Clause is Undecidable},
  author = {Philippe Devienne and Patrick Lebègue and Jean-Christophe Routier},
  year = {1993},
  researchr = {https://researchr.org/publication/DevienneLR93},
  cites = {0},
  citedby = {0},
  pages = {48-57},
  booktitle = {STACS 93, 10th Annual Symposium on Theoretical Aspects of Computer Science, Würzburg, Germany, February 25-27, 1993, Proceedings},
  editor = {Patrice Enjalbert and Alain Finkel and Klaus W. Wagner},
  volume = {665},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-56503-5},
}