部分例示手法に基づく定理自動証明に関する研究

この論文をさがす

著者

    • 山本, 雅人 ヤマモト, マサヒト

書誌事項

タイトル

部分例示手法に基づく定理自動証明に関する研究

著者名

山本, 雅人

著者別名

ヤマモト, マサヒト

学位授与大学

北海道大学

取得学位

博士 (工学)

学位授与番号

甲第3858号

学位授与年月日

1996-03-25

注記・抄録

博士論文

v, 96p.

Hokkaido University(北海道大学). 博士(工学)

目次

  1. 目次 / p1 (0003.jp2)
  2. 1 序論 / p1 (0008.jp2)
  3. 1.1 背景 / p1 (0008.jp2)
  4. 1.2 本研究の目的 / p3 (0010.jp2)
  5. 2 記号論理の基礎 / p6 (0013.jp2)
  6. 2.1 命題論理 / p7 (0014.jp2)
  7. 2.2 第一階述語論理 / p14 (0021.jp2)
  8. 3 定理自動証明に対するこれまでの手続き / p29 (0036.jp2)
  9. 3.1 導出原理 / p30 (0037.jp2)
  10. 3.2 部分例示手法 / p35 (0042.jp2)
  11. 4 部分例示手法に基づく定理自動証明手続き / p43 (0050.jp2)
  12. 4.1 諸定義 / p44 (0051.jp2)
  13. 4.2 手続きの詳細 / p47 (0054.jp2)
  14. 4.3 完全性の証明 / p57 (0064.jp2)
  15. 4.4 例題 / p60 (0067.jp2)
  16. 5 手続きの効率化 / p64 (0071.jp2)
  17. 5.1 効率化の要点 / p65 (0072.jp2)
  18. 5.2 実験および考察 / p72 (0079.jp2)
  19. 6 結論 / p79 (0086.jp2)
  20. 6.1 各章の要約 / p79 (0086.jp2)
  21. 6.2 まとめ / p81 (0088.jp2)
  22. 謝辞 / p83 (0090.jp2)
  23. 参考文献 / p84 (0091.jp2)
  24. A プログラムリスト / p88 (0095.jp2)
  25. A.1 Davis-Putnamの手続き / p88 (0095.jp2)
  26. A.2 部分例示手法に基づく定理自動証明手続き / p91 (0098.jp2)
1アクセス

各種コード

  • NII論文ID(NAID)
    500000132860
  • NII著者ID(NRID)
    • 8000000967450
  • DOI(NDL)
  • 本文言語コード
    • jpn
  • NDL書誌ID
    • 000000297174
  • データ提供元
    • 機関リポジトリ
    • NDL-OPAC
    • NDLデジタルコレクション
ページトップへ