@techreport{oai:ipsj.ixsq.nii.ac.jp:00033603,
 author = {吉田, 忠行 and 赤間, 清 and 宮本, 衛市 and Tadayuki, Yoshida and Kiyoshi, Akama and Eiichi, Miyamoto},
 issue = {76(1999-MPS-026)},
 month = {Sep},
 note = {論理プログラミングの理論では,当初は確定節で問題を表現していた.その後,否定の表現を取り入れ,さらには,否定を含む確定節を基礎として,一階述語論理の表現も確定節のボディで扱うことができるようになった.しかし論理プログラミングは,このような一階述語論理を含む確定節で表現されたプログラムを計算することに関して,正当性と柔軟性に問題を抱えている.本論文では,この問題を解決するために,等価変換パラダイムを採用する.等価変換の枠組で一階述語論理の表現を扱うために,一階論理制約の概念を導入する.一階論理制約とは,基本的な制約を論理記号によって組み立てた複合的な制約である.まず,一階論理制約の表現を定義し,その表現に対する意味を与える.そして,一階論理制約のための等価変換ルールを提案し,その正当性を証明する., In the theory of logic programming, the class of definite clauses was adopted first. Then the concept of logic programs was extended to include negative literals and arbitrary first-order formulas in the body of definite clauses. Computation of first-order expressions has, however, some difficulties with respect to the correctness and the flexibility. In this paper, the equivalent transformation paradigm (ET paradigm) is adopted to overcome these difficulties. We introduce first-order logical constraints, which are compound constraints composed of basic constraints constructed using logical connectives and quantifiers. We define the class of FLCs and determine the meaning of them. Next, we propose ET rules for FLCs and prove the correctness of these rules.},
 title = {一階論理表現の等価変換を用いた問題解決の正当性},
 year = {1999}
}