論理体系CLCを用いた定理証朋支援システムにおけるアラー分解方法の提案
スポンサーリンク
概要
- 論文の詳細を見る
定理証明支援システムを考える上で、最も困難な問題の1つとして、アラー分解が挙げられる。アラー分解は他の分解と異なり、何回でも分解することが可能で、分解したからといって必ずしも証明を1歩前進させることにはならない。さらに、いたずらにアラー分解をすれば単に時間がかかるだけでなく、恒真の判定の際に必要となるシーケントの左右の比較の量を増やし、メモリーの使用量を増やし、アラー変数の代入の可能性を増やすことになる。そこで、できるだけ必要のないアラー分解を避けて、証明の方針を見つけやすくする方法の1つとして、我々は本論文において、どのアラー分解をいつ行なうのかを、ユーザと協調して行なう方法を提案する。
- 一般社団法人情報処理学会の論文
- 1995-03-15
著者
関連論文
- 発達障害児・者へのパニック対応学習支援システムの開発I : パニック・リフレクションモデルの開発と可能性(自主シンポジウム18,日本特殊教育学会第47回大会シンポジウム報告)
- 自閉症児のパニック行動に対する情報技術による支援
- 児童生徒の操作履歴を基に自動採点を行う試験システムの開発
- D-15-25 類似検索技術を応用した学術論文情報配信システム
- Definition of the Mongolian Character Codesets Enabling Multilingual Text Manipulation
- 情報教育の音楽化による高校生へのプログラミング入門
- 「情報B」の教科書比較 : 「手順的な自動処理」の観点から
- ACM SIGUCCS Fall 2005 Conference参加報告 : 北米における大学ITインフラ支援の状況(会場A)
- ACM SIGUCCS Fall 2005 Conference参加報告
- 情報倫理教育の国際比較
- 放送大学における情報教育
- 情報倫理教育に関する国外の状況調査 : 教材の国際的共同開発のために(インターネットと情報教育-シングルセッション,インターネットと情報倫理教育,一般)
- 情報倫理教育に関する国外の状況調査 : 教材の国際的共同開発のために(インターネットと情報教育-シングルセッション,インターネットと情報倫理教育,一般)
- 情報倫理教育に関する国外の状況調査 : 教材の国際的共同開発のために(インターネットと情報倫理教育-シングルセッション,インターネットと情報倫理教育,一般)
- BS-11-5 大学の情報セキュリティ強化と情報倫理ビデオ(BS-11.進化するキャンパス情報システムとセキュリティ対策・情報倫理教育,シンポジウムセッション)
- 情報倫理ビデオの製作と大学の情報セキュリティへの応用(セキュリティ,サービス管理,ビジネス管理,料金管理,及び一般)
- 情報倫理ビデオの製作と大学の情報セキュリティへの応用(セキュリティ,サービス管理,ビジネス管理,料金管理,及び一般)
- 高機能自閉症児のための絵記号コミュニケーション学習支援の実践(障害者教育・特別支援教育)
- 自閉症者の学習を支援するPDA用汎用ソフトウェアの開発と評価
- 情報科教育法における情報倫理とモラル(インターネットと情報教育-シングルセッション,インターネットと情報倫理教育,一般)
- 情報科教育法における情報倫理とモラル(インターネットと情報教育-シングルセッション,インターネットと情報倫理教育,一般)
- 情報科教育法における情報倫理とモラル(インターネットと情報倫理教育-シングルセッション,インターネットと情報倫理教育,一般)
- 情報科教育法の知識体系
- 情報科教員の卵を育てる 情報科教育法で教師としての責任感を
- 教科「情報」における情報フルーエンシーとその実践
- AP-1-2 大学等における情報セキュリティポリシーの教育・普及・研修について(AP-1. リスクマネジメント中心の情報セキュリティ,パネルセッション,ソサイエティ企画)
- 情報倫理ビデオ教材の開発指針 : 使いやすい授業素材と学習者の自主学習に向けて
- 英語授業におけるコンピュータ・リテラシの付随的獲得
- 情報科教員養成における情報倫理とモラルの取扱
- Moodleを利用した論文査読システムの試み
- 情報倫理ビデオ教材のプレポストテストによる評価(技術者倫理・情報倫理教育の現状と課題,及び一般)
- 考えさせる情報倫理教育ビデオとその評価(サービス管理,ビジネス管理,料金管理,及び一般)
- 考えさせる情報倫理教育ビデオとその評価(サービス管理・ビジネス管理,料金管理,及び一般)
- 大学生向け情報倫理ビデオ教材の作成と効果
- 教科「情報」における車型ロボットの利用
- 情報フルーエンシーを意識した大学の一般情報教育のカリキュラム提案
- 「教育用プログラミング言語に関するワークショップ2006」の報告
- ドリトルと「情報教育の音楽化」
- 対面での応答を重視した英語学習活動と発話収録装置の試作と試用
- リテラシとしてのプロジェクト管理
- 学習履歴の双対性再考 : 英語語彙学習履歴のマイニングに向けて
- 学習履歴の双対性 : 学習履歴を活用したe-learning高度化の数理的基礎を目指して
- 語学教育の情報化
- 「情報教育」の情報化
- 「情報教育」と「教科教育の情報化」
- 新しい「情報倫理」の目指すもの (人文科学とコンピュータ)
- 情報倫理教育と学生の実状
- 情報倫理教育における映像教材の国際化(技術者倫理・情報倫理教育の現状と課題,及び一般)
- 情報危機管理と情報倫理教育
- 情報倫理教育における情報フルーエンシー(ソーシャル・ネットワークと情報教育関係)
- 新・試作教科書「情報IIIx」と他分野との関連(特別セッション 情報処理学会高校普通教科「情報」新・試作教科書)
- 初等中等教育における情報倫理教育のあり方について
- WWWを用いた情報発信教育について
- 多様なワークフローを考慮したmoodle上での予約モジュールのデザイン
- 「新・試作教科書」における情報社会/情報倫理の扱い(特別セッション 情報処理学会高校普通教科「情報」新・試作教科書)
- 6.教育用プログラミング言語を利用した教科教育と情報教育(教育用プログラミング言語と授業利用)
- 利用者教育としてのspamメール対策
- 母関数を用いたプログラム変換
- 自閉症児教育のためのコミュニケーション支援ツールの作成と評価
- 論理体系CLCを用いた定理証朋支援システムにおけるアラー分解方法の提案
- ネットビジネス業者の「プライバシー保護対策」評価の提案
- HTMLをもちいた定理の自動証明システムの実現
- N-31 教育機関におけるネットワーク運用規約作成支援システムの設計(教育支援システム(2),N.教育・人文科学)
- 個人情報保護法のキモチ (特集 個人情報保護と図書館)
- 情報フルーエンシーと情報処理学会GEBOK
- 教科「情報」の大学入試への導入の現状と展望
- Are You Ready?--教科「情報」の準備はできていますか?
- 情報教育の音楽化
- ヒトゲノム解読技術の発達とプライバシー (HUMANOMEプロジェクト)
- 情報倫理と情報危機管理の視点から考えるメディアリテラシー教育 (特集 メディアリテラシーという視点--情報教育に求められていくもの)
- 5X-8 情報教育のためのソフトウエア環境への要件 : 情報危機管理教育をめざして
- 3L-3 WWWで利用できる計算次数測定システム
- 実験的手法による計算量の測定
- ランダムデータサーバーを用いた計算時間の推定と検定
- 教育現場における情報通信倫理教育
- 教育改革とインターネットによる情報発信
- 論理体系CLCを用いた定理証明支援システムにおけるアラー変数代入方法の提案
- Linear Logicと島内剛一のProver CLC
- 大学生の情報倫理にかかわる判断と行動