述語論理における証明手続について : Theorem Prover TP-I
スポンサーリンク
概要
- 論文の詳細を見る
This paper treats the proof procedure of the first order predicate calculus. At frist, a proof procedure (named BPP) of Gentzen's LK type logic system is shown to be complete. It is also shown that several cases of decision problems in the predicate calculus are solved by using the the completeness of BPP. Then an effcient decision procedure (named DAIM) for these cases is proposed. Finally Theorem Prover TP-I is described, which is the implementatlon of the combined procedure of DAIM and MPP (the modified procedure of BPP).
- 一般社団法人情報処理学会の論文
- 1973-02-15
著者
関連論文
- 仮想マシンモニタによる仮想マシン内プロセスの制御(OS-2 : セキュリティ)
- 階層的コレクションに基づくオブジェクト指向分散ライブラリについて
- 並列オブジェクト指向言語のマルチコンピュータ上における効率的な実装法
- B-033 SoftwarePotへのチェックポイント機構の導入(B.ソフトウェア)
- 仮想実行環境を管理するためのライブラリ(ポスターセッション)
- サンドボックスシステムにおける投機的な安全性検査(セキュリティ)
- John Backus : Can Programming Be Liberated from the von Neumann Style ? A Functional Style and its Algebra of Programs(20世紀の名著名論)
- 79-19 プログラミングは von Neumann スタイルから解放されうるか?関数的スタイルとそのプログラムの代数
- 述語論理における証明手続について : Theorem Prover TP-I
- 接続を動的に制御するメッセージパッシングシステム(HPC-11 : グリッド(3))(2004年並列/分散/協調処理に関する『青森』サマー・ワークショップ(SWoPP青森2004) : 研究会・連続同時開催)
- Virtual Private Grid(VPG) : 遠隔計算機を効率的に利用するシェル
- オブジェクト指向言語によって記述された, 携帯電話, PDAのアプリケーションプログラム圧縮方式
- 分散記憶並列計算機における局所ごみ集めのスケジュール方式について(並列処理)
- 最小限のコンパイラサポートによる細粒度マルチスレッディング : 効率的なマルチスレッド言語を実装するためのコスト効率の良い方法(並列処理)
- 分散メモリ並列計算機におけるReference count GCとMark and Sweep GCの比較