WEKO3
-
RootNode
アイテム
一階論理表現の等価変換を用いた問題解決の正当性
https://ipsj.ixsq.nii.ac.jp/records/33603
https://ipsj.ixsq.nii.ac.jp/records/33603a823e6dc-989b-4720-88b5-02c664bec0cd
名前 / ファイル | ライセンス | アクション |
---|---|---|
![]() |
Copyright (c) 1999 by the Information Processing Society of Japan
|
|
オープンアクセス |
Item type | SIG Technical Reports(1) | |||||||
---|---|---|---|---|---|---|---|---|
公開日 | 1999-09-21 | |||||||
タイトル | ||||||||
タイトル | 一階論理表現の等価変換を用いた問題解決の正当性 | |||||||
タイトル | ||||||||
言語 | en | |||||||
タイトル | The Correctness of Problem Solving using Equivalent Transformation of First - order Logical Expressions | |||||||
言語 | ||||||||
言語 | jpn | |||||||
資源タイプ | ||||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
資源タイプ | technical report | |||||||
著者所属 | ||||||||
北海道大学大学院システム情報工学専攻 | ||||||||
著者所属 | ||||||||
北海道大学情報メディア教育研究総合センター | ||||||||
著者所属 | ||||||||
北海道大学大学院システム情報工学専攻 | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Division of System and Information Engineering, Hokkaido University | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Center of Infomation and Multimedia Studies, Hokkaido University | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Division of System and Information Engineering, Hokkaido University | ||||||||
著者名 |
吉田, 忠行
赤間, 清
宮本, 衛市
× 吉田, 忠行 赤間, 清 宮本, 衛市
|
|||||||
著者名(英) |
Tadayuki, Yoshida
Kiyoshi, Akama
Eiichi, Miyamoto
× Tadayuki, Yoshida Kiyoshi, Akama Eiichi, Miyamoto
|
|||||||
論文抄録 | ||||||||
内容記述タイプ | Other | |||||||
内容記述 | 論理プログラミングの理論では,当初は確定節で問題を表現していた.その後,否定の表現を取り入れ,さらには,否定を含む確定節を基礎として,一階述語論理の表現も確定節のボディで扱うことができるようになった.しかし論理プログラミングは,このような一階述語論理を含む確定節で表現されたプログラムを計算することに関して,正当性と柔軟性に問題を抱えている.本論文では,この問題を解決するために,等価変換パラダイムを採用する.等価変換の枠組で一階述語論理の表現を扱うために,一階論理制約の概念を導入する.一階論理制約とは,基本的な制約を論理記号によって組み立てた複合的な制約である.まず,一階論理制約の表現を定義し,その表現に対する意味を与える.そして,一階論理制約のための等価変換ルールを提案し,その正当性を証明する. | |||||||
論文抄録(英) | ||||||||
内容記述タイプ | Other | |||||||
内容記述 | 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. | |||||||
書誌レコードID | ||||||||
収録物識別子タイプ | NCID | |||||||
収録物識別子 | AN10505667 | |||||||
書誌情報 |
情報処理学会研究報告数理モデル化と問題解決(MPS) 巻 1999, 号 76(1999-MPS-026), p. 45-48, 発行日 1999-09-21 |
|||||||
Notice | ||||||||
SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
出版者 | ||||||||
言語 | ja | |||||||
出版者 | 情報処理学会 |