証明力が拡張された適切さの論理体系ER

• Item type: National Convention(1)
• 公開日: 1997-09-24
• タイトル: 証明力が拡張された適切さの論理体系ER
• タイトル / 言語: en
• タイトル: Relevant logic ER, the extended system R
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: 東京工業大学情報理工学研究科計算工学専攻
• 著者所属: 東京工業大学情報理工学研究科計算工学専攻
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Tokyo Institute of Technology
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Tokyo Institute of Technology
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 論理の主たる目的は, 人間の行なう演繹的な推論を形式化することである。しかし, 古典論理における含意「ならば」は, 日常利用する「ならば」とは, 違和を感じる箇所もある。例えば, 古典論理では, 「2+3=5」が真であることから, 「雪は白いならば, 2+3=5」が真となる。しかし, このような推論は, 奇異に感じられる。古典論理の含意が持つこのような違和感は次のように3つに分類される。1. 関連性の違和感 A→(B→A), 2. 恒真性の違和感 (A∧￢A)→B, A→(B∨￢B), 3. 偶然性の違和感 A→((A→B)→B)。適切さの論理は, これらの違和感を除去することを目的として研究されてきた。Lewisによる関連性の違和感が除去された厳密含意の提案に始まり, 多くの適切さの論理の体系が提案されている。代表的な体系としては, ChurchやMohによる, 関連性と恒真性の違和感が除去された論理体系Rや, Ackennannによる, すべての違和感が除去された論理体系Eなどがある。関連性・恒真性の違和感は強い違和感とみなされ, ほとんどの体系で, これらは除去されている。一方, 適切さの論理では, 体系が弱いという問題がある。例えば, 自然演繹における推論規則Disjunctive syllogism (DS)が許されない。[numerical formula]この推論規則が認められない理由は, 以下のように(A∨￢A)+Bが証明可能となるためである。[numerical formula][5]では, DSが問題のある規則と見なされ, 適切さの論理では, この推論規則は除去されている。また, 違和感を含んでいない以下の式が, 適切さの論理では定理ではない。1. A→(B→(A∧B)), 2. A→(A∧(B∨￢B))。適切さの論理では, 1.が定理である場合, A→(B→A)が定理となり, また, 2.が定理である場合, A→(B∨￢B)が定理となるため, これら2つの式は定理とはならない。このように, 適切さの論理では, 違和感を除去するために, 結果として, 定理となることが自然であると考えられる式が定理とはならず, また, 自然な推論規則が成り立たない。本稿では, 関連性・恒真性の違和感が除去されており, 体系Rよりも強い論理体系ERを提案する。ERは, [4]に示されているsequentによる自然演繹の体系として与えられ, 各推論規則では, 式の属性が利用される。この属性は, 証明を制御し, 違和感を含む式の推論を防ぐために利用される。また, 属性を利用する点からみると, ERは, Labelled deductive systemの一種であるといえる。
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00349328
• 書誌情報: 全国大会講演論文集; 巻 第55回, 号 人工知能と認知科学, p. 553-554, 発行日 1997-09-24
• 出版者 / 言語: ja
• 出版者: 情報処理学会