Core Concepts
論理プログラムP、Qと許可された述語集合Vが与えられた場合、PとQが強く等価になるようなプログラムRを効果的に構築できる。これは、第一階論理の Craig 補間を用いて実現できる。
Abstract
本論文では、論理プログラムの強い等価性を第一階論理の等価性として表現し、Craig 補間を用いて効果的に定義可能なプログラムRを構築する手法を提案している。
まず、論理プログラムを第一階論理の式で表現する方法を示し、その式が論理プログラムを表現しているかどうかを判定する基準を定義する。この基準に基づいて、与えられた第一階論理の式から論理プログラムを抽出する手順を示す。
次に、与えられた論理プログラムP、Qと許可された述語集合Vについて、PとQが強く等価になるようなプログラムRを構築する手法を提案する。これは、P、Qの第一階論理の表現とVに基づいて、Craig 補間を用いて効果的に行うことができる。
さらに、述語の出現位置(正の頭部、負の頭部、正の本体、負の本体)を制限することで、より細かな制御が可能な手法も示している。
この手法は、知識表現の高度な課題において重要な役割を果たす定義可能性と補間の概念を、答案集合プログラミングに適用したものである。
Stats
論理プログラムP、Qと許可された述語集合Vが与えられた場合、PとQが強く等価になるようなプログラムRを効果的に構築できる。
述語の出現位置を制限することで、より細かな制御が可能。
Quotes
"我々は、安定モデル意味論の下での論理プログラムの強い等価性を古典的な論理式の等価性に翻訳できることを示す。"
"与えられたプログラムPとQに対して、与えられた語彙Vの中で、PとQが強く等価になるようなプログラムRを自動的に合成することが我々の目的である。"
"我々の結果は効果的である: Craig 補間から得られる式からプログラムRを構築できる。"