[Updated on Apr. 18] Integration of CiNii Articles into CiNii Research


Bibliographic Information

Other Title
  • ドウシュツギ カラノ ループ ケンシュツ ニ ヨル ロンリ プログラム ノ ヒテイシセイ ショウメイホウ
  • Proving Non-termination of Logic Programs by Detecting Loops in Derivation Trees

Search this article


In this paper, we present a method for automatically proving non-termination of logic programs. Given a program and a question pattern, the method proves non-termination by detecting a loop in the derivation tree constructed from the question that represents an arbitrary questions for the question pattern. For soundness, we distinguish variables given as arguments of predicates, and we keep the distinction in the derivation. We also report an implementation of the method, and compare it with other tools by applying it to programs in LP category of Termination Competition 2007.



See more


Report a problem

Back to top