導出木からのループ検出による論理プログラムの非停止性証明法

Bibliographic Information

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

Search this article

Abstract

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.

Journal

References(12)*help

See more

Details 詳細情報について

Report a problem

Back to top