拡張論理プログラムへの意味論的関係に基づく変換による優先順位付き極小限定の計算  [in Japanese] Computing Prioritized Circumscription by Compiling into Extended Logic Programs Based on the Semantic Relationship  [in Japanese]

We propose a method of compiling circumscription into extended logic programs which is widely applicable to a class of parallel circumscription as well as a class of prioritized circumscription. In this paper, we show theoretically that circumscription whose theory contains both the domain closure axiom and the uniqueness of names axioms and does not contain function symbols can be compiled into an extended logic program II, so that, whether a ground literal is provable from circumscription or not, can be evaluated by deciding whether the literal is true in all answer sets of II, which can be computed by running II under the existing logic programming interpreter. The proofs of all theorems w.r.t. the method are also presented.