適切さと論理RとERの証明力の比較
スポンサーリンク
概要
- 論文の詳細を見る
The formalization of human deductive reasoning is a main issue in artificial intelligence. Although classical logic (CL) is one of the most useful ways for the formalization, the implication of CL has some fallacies. For example, in Cl, A→B can be inferred form B for and arbitrary formula A. This inference is incorrect from the viewpoint of the meaning of implication which human has. In human deductive reasoning, when A⇾B is inferred, A and B should be related. Relevant logic has been studied for removal of implication fallacies in CL. The system R is a typical logical system from which fallacies of relevance and validity are removed. ER is a relevant typical logical system from which fallacies of relevance and validity are removed. ER is a relevant logical system from which these fallacies are removed and this system is not weaker than R. Especially, it is known that disjunctive syllogism holds in ER but does not hold in R. This inference rule is considered to be natural in human reasoning. In this paper, we prove that ER is properly stronger than R. This means that, for the formalization of human deductive reasoning, ER is more suitable than other relevant logical systems. The proof consists of the following steps: First, the natural deduction systems FR and FR' are introduced. FR is a natural deduction system equivalent to R. It is proved that FR' is stronger than FR. Next, we show that he normalization theorem holds in FR' and that there is a proof of ER corresponding to each normal proof of FR'. In addition, We show the fact that there is theorem of ER which can not be inferred in R. It follows that ER is properly stronger than R.
- 社団法人人工知能学会の論文
- 1999-11-01
著者
-
米崎 直樹
東京工業大学大学院情報理工学研究科計算工学専攻
-
吉浦 紀晃
埼玉大学大学院理工学研究科数理電子情報部門情報領域
-
吉浦 紀晃
東京工業大学情報理工学研究科計算工学専攻
-
吉浦 紀晃
埼玉大学大学院工学研究科
-
米崎 直樹
東京工業大学大学院情報理工学研究科
関連論文
- 記号論的暗号解析を用いたOblivious Transferプロトコルの解析(セキュリティ,フォーマルアプローチ論文)
- 記号論及び計算論によるセキュリティ解析の相互関係(数理的技法による情報セキュリティ)
- 利他主義と情報技術による地域社会の安全化 : e自警ネットワーク実現に向けたシステムの導入と展望(第4部 学術論文,ユビキタス社会と建築・都市のフロンティア)
- 移動体通信システムにおける移動体の動きと通信性能評価に関する研究
- 証明力が拡張された適切さの論理体系ER
- 線形論理CLL_eのモデルを用いた意味論
- 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法(セッション4-B : ネットワークセキュリティ(1))
- 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法
- 大学における情報化戦略と理工系情報学科の貢献
- 様相記号列統一化による様相論理定理証明器における自己代入の利用
- 様相記号列統一化による様相論理定理証明器の健全性と完全性
- 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法(セッション4-B : ネットワークセキュリティ(1))
- 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法
- 移動体の移動を考慮した二次元セルラーネットワークの性能評価
- 一次元セルラーネットワークにおける保留時間を考慮したチャネル制御について(通信と制御)
- 二次元セルラーシステムにおける移動特性と通信性能に関するシミュレーション評価
- 分割アルゴリズムに基づく同型グラフの検索について
- リスト構造に対する整合機能の形式化
- ソフトウェア科学会第1回大会
- 自然言語に基づく静的システムの仕様のプロトタイププログラムへの変換手法
- 分散自律設置カメラシステムによる地域社会の安全化--e自警ネットワーク構想の概要と学校への導入事例紹介 (第22回センシングフォーラム 資料--センシング技術の新たな展開と融合) -- (セッション1B2 ネットワークセンシングシステム)
- 画像の構造情報の抽出とその応用
- 形式オントロジーに基づく遺伝子調節のための数値モデル
- 演繹体系による暗号方式の形式化と体系の性質としての暗号方式の安全性
- 演繹体系による暗号方式の形式化と体系の性質としての暗号方式の安全性
- Spi計算の型付けによる公開鍵暗号方式を用いたプロトコルのメッセージ認証の検証
- 初等的でないフレームを持つ様相論理の統一化による証明法
- 一次元セルラーネットワークの通信性能に関する移動体の速度分布の影響について(プロトコルと開発ツール)(新時代の分散処理とネットワーク(WebサービスとP2P))
- 生体情報による認証への一方向関数の応用
- 移動体の速度分布を考慮した一次元セルラーネットワークのシミュレーションによる通信性能評価
- ハッシュ関数を用いた生体情報による認証の実験
- ハッシュ関数を用いた生体情報による認証の実験
- ハッシュ関数を用いた生体情報による認証の実験
- 多地点参加の遠隔講義の運用実験
- 多地点参加の遠隔講義の運用実験
- 適切さの論理ERの自動定理証明器の実装 (特集 「知識発見の生命科学への応用」および一般)
- 導出法による線形論理CLL_eの自動証明戦略
- オブジェクトの項表現を意味論の基礎とする論理体系としてのOntologyとその表現力
- BitTorrentにより配信される音楽や映像ファイルの自動検出 (インターネットアーキテクチャ)
- BitTorrentにより配信される音楽や映像ファイルの自動検出 (技術と社会・倫理)
- リアクティブシステムの仕様記述言語とその記述操作の特徴付け
- 時相論理を用いた試験等価性の特性化
- 産業界からの理工系情報学科の研究教育内容への期待と大学の取り組み
- 大学における情報化戦略と理工系情報学科の貢献(パネル討論)
- DNSサーバの分散管理から集中管理への移行 (第4回ネットワークシンポジウム講演論文集)
- 時相論理によるリアクティブシステム動作仕様からの効率的なプログラムの合成法 (第3回ネットワークシンポジウム講演論文集)
- 20周年記念特集号の編集にあたって(20周年記念特集)
- 時間論理によるリアクティブシステム仕様の検証の効率化(セキュアコンピューティング)
- SSLとリレーサーバを用いたPOP before SMTPのセキュアな実現法
- リアクティブシステムの段階的充足可能性とSafety Propertyの関係
- セキュリティプロトコルにおける暗号化メッセージの送信者による認知に関する検証法
- セキュリティプロトコルの一貫性および正常終了一致の同一参加者による複数セッションを考慮した検証法
- セキュリティプロトコルの一貫性および正常終了一致の検証法
- セキュリティプロトコルの一貫性および正常終了一致の検証法
- 自然言語の語彙分割による形式的仕様記述
- 合成可能なタブローによる仕様の差分的無矛盾性判定について (プログラム変換と記号・数式処理)
- 証明力を拡張した適切さの論理$ER$ (プログラム変換と記号・数式処理)
- 適切さと論理RとERの証明力の比較
- 適切さの論理ERの決定可能性
- 証明力を拡張した適切さの論理ER
- 大学における情報科学教育とリテラシー教育
- 欠陥仕様からの修正情報抽出に関する研究
- 合成可能な時間論理タブローの構成法
- 結合子の適切さによる人間の演繹的な推論の形式化 (&特集>「記号論理とAI」)
- 普通のUntil演算子を持つ命題実時間論理について
- 時相論理による段階的仕様記述プロセスに対応した検証法
- 証明の失敗から得られる情報を用いる様相論理定理証明戦略
- 時相論理による仕様記述の無矛盾性判定のための再利用可能なタブローについて
- BitTorrentにより配信される音楽や映像ファイルの自動検出
- プライベートネットワークアドレスを利用する際の経路制御について
- 紛失通信プロトコルの解析のための可能世界意味論に基づく形式体系
- リアクティブシステム動作仕様の段階的充足可能性の判定手続き(システム検証の科学技術)
- DNSサーバの分散管理から集中管理への移行
- リアクティブシステムの利用に伴う進化
- ソフトウェア発展と検証技術の未来 (特集 ソフトウェア発展)
- オブジェクトの生成,消滅を表現可能な論理体系DOL
- オブジェクトの生成、消滅を表現可能な論理体系DOL
- 様相論理 (<特集>非標準論理とその応用)
- The Temporal Semantics of Logic Programming
- Access Control Listの等価性判定のためのテストケース生成 (技術と社会・倫理)
- ICMPパケットの遮断によるIPv6通信における問題への対策 (情報通信マネジメント)
- Access Control Listの等価性判定のためのテストケース生成 (インターネットアーキテクチャ)
- 災害対策におけるコミュニケーション基盤フレームワークの一提案(省エネルギーと超高速ネットワーク,インターネットと環境・エコロジー,一般)
- 時相論理によるリアクティブシステム仕様の実現可能性に関する分類 (21世紀のソフトウェア工学)
- 災害対策におけるコミュニケーション基盤フレームワークの一提案
- 首都圏近郊の大学における計画停電の影響と対策
- Access Control Listの等価性判定のためのテストケース生成(NW情報調査・可視化技術,インターネットと情報倫理教育,一般)
- Access Control Listの等価性判定のためのテストケース生成(NW情報調査・可視化技術,インターネットと情報倫理教育,一般)
- ICMPパケットの遮断によるIPv6通信における問題への対策(サービス管理,運用管理技術,セキュリティ管理,及び一般)
- 検索されたWebページにおける検索語に基づく重要箇所の表示(ネットワークサービス,インターネットと情報倫理教育,一般)
- 位置情報に基づく災害時の重要情報を優先転送するネットワーク管理手法〜実用化に向けた実地検証報告〜