On computer aided mathematical reasoning コンピュータによる数学的論証の支援について

この論文をさがす

著者

    • 坂井, 公, 1953- サカイ, コウ

書誌事項

タイトル

On computer aided mathematical reasoning

タイトル別名

コンピュータによる数学的論証の支援について

著者名

坂井, 公, 1953-

著者別名

サカイ, コウ

学位授与大学

東京工業大学

取得学位

理学博士

学位授与番号

乙第2120号

学位授与年月日

1990-11-30

注記・抄録

博士論文

目次

  1. 論文目録 / (0002.jp2)
  2. Contents / p2 (0005.jp2)
  3. 0. Introduction / p1 (0007.jp2)
  4. 1. Preliminaries / p7 (0010.jp2)
  5. 1.1 Reduction system / p7 (0010.jp2)
  6. 1.2 First-order language / p9 (0011.jp2)
  7. 1.3 Logic programming / p13 (0013.jp2)
  8. 1.4 Term rewriting system / p16 (0015.jp2)
  9. 2. Well-founded order on terms / p20 (0017.jp2)
  10. 2.1 Properties of well-founded orders on terms / p20 (0017.jp2)
  11. 2.2 Lexicographic subterm ordering / p21 (0017.jp2)
  12. 3. An equational unification procedure / p24 (0019.jp2)
  13. 3.1 Equational unification problems / p24 (0019.jp2)
  14. 3.2 Inference rules for equational unification / p26 (0020.jp2)
  15. 3.3 Completeness of the unification procedure / p29 (0021.jp2)
  16. 3.4 Implementation issues and examples / p34 (0024.jp2)
  17. 4. Complete inference for cancellation axiom / p37 (0025.jp2)
  18. 4.1 Inference rules for cancellation / p37 (0025.jp2)
  19. 4.2 Well-founded order on atomic formulas / p38 (0026.jp2)
  20. 4.3 Completeness of the inference rules / p41 (0027.jp2)
  21. 4.4 Cancellation in richer algebraic structure / p46 (0030.jp2)
  22. 5. Constraint logic programming / p49 (0031.jp2)
  23. 5.1 CLP on many-sorted algebra / p49 (0031.jp2)
  24. 5.2 Least fixed point semantics of CLP / p51 (0032.jp2)
  25. 5.3 Operational semantics of CLP / p52 (0033.jp2)
  26. 5.4 Constraint solving and canonical forms / p54 (0034.jp2)
  27. 5.5 An algebraic constraint solver / p55 (0034.jp2)
  28. 5.6 A Boolean constraint solver / p59 (0036.jp2)
  29. 6. Natural handling of negation / p62 (0038.jp2)
  30. 6.1 Pure prolog with negation (PPN) / p63 (0038.jp2)
  31. 6.2 Execution of PPN as a programming language / p64 (0039.jp2)
  32. 6.3 PPN and intuitionistic logic / p67 (0040.jp2)
  33. 6.4 Knowledge assimilation on PPN / p70 (0042.jp2)
  34. 7. Definite clause grammar and bottom-up parsing / p73 (0043.jp2)
  35. 7.1 Definite clause grammar / p73 (0043.jp2)
  36. 7.2 Semantics of DCG / p75 (0044.jp2)
  37. 7.3 Top-down DCG translation / p76 (0045.jp2)
  38. 7.4 Bottom-up DCG translation / p77 (0045.jp2)
  39. 7.5 Efficient bottom-up translation / p80 (0047.jp2)
  40. References / p87 (0050.jp2)
0アクセス

各種コード

  • NII論文ID(NAID)
    500000078107
  • NII著者ID(NRID)
    • 8000000998635
  • DOI(NDL)
  • NDL書誌ID
    • 000000242421
  • データ提供元
    • NDL-OPAC
    • NDLデジタルコレクション
ページトップへ