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

書誌事項

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

この論文をさがす

抄録

本稿では,論理プログラムの非停止性を自動的に証明する手法を提案する.本手法では,与えられた質問パターンを代表する質問から起こり得る導出を木で構成し,その木の中からループを検出することにより質問パターンに対する非停止性を示す.具体的には,質問パターンの入力と出力を変数に置き換えた質問から導出木を構成するが,その導出やループ検出の際に入力に対応する変数を特別扱いすることにより健全性を確保する.実際に本手法を実現したツールを作成し,Termination Competition 2007の論理プログラム部門で与えられているサンプルプログラムを対象とした実験を行い,既存の研究との比較を行う.

収録刊行物

参考文献 (12)*注記

もっと見る

詳細情報 詳細情報について

問題の指摘

ページトップへ