TPTP

[数学,機械学習,東ロボ,Prolog]

TPTP

• TPTP Technical Report

TPTPはPrologで書かれた自動定理証明のためのライブラリ。

追記: 自動定理証明や単純な代数計算に関しては、もっと新しいものや手軽に使えるSageMathのようなものを使った方がいい気がする

  事始め

• Prologのインストール Prolog入門 はここで

The TPTP World Tutorial を読んでいく

What is Automated Reasoning?(自動推論とは何ですか？)

• 世界の問題を論理に変換する
  • 公理(Axioms)はあなたが世界について知っていることを説明します
  • 予想(Conjecture)は何を解決する必要があるかを説明します
• 論理解決策を得るために自動推論を使用する
  • 自動証明器(theorem prover)は証明を見つける
  • モデルファインダー有限カウンターモデル
  • モデルファインダーは公理が一貫していることを確認します
• 論理解決策を世界に翻訳する
  • 予想の証明は解決策を説明します
  • カウンターモデルは、解決策がない理由の例です

筆者注

theorem prover(自動証明器)と呼ばれるものは世界にいくつもあるようだ SystemOnTPTP の画面左側にあるもので、GitHubへのリンクがあったりするが、それらがすべて自動証明器。 TPTPはそのファイルフォーマットを定めていると言える

  TPTPのインストール

Getting and Using the TPTP

• TPTPのトップページでTPTP-v7.5.0.tgzをDLできる

// tsh, tcshをインストールする
$ sudo apt-get install tsh tcsh

// TPTPをインストールする
$ wget http://www.tptp.org/TPTP/Distribution/TPTP-v7.5.0.tgz -O ~/Downloads/TPTP-v7.5.0.tgz
$ sudo tar xvf TPTP-v7.5.0.tgz -C /opt
$ sudo chown {一般ユーザー名}:{一般ユーザー名} /opt/TPTP-v7.5.0/
$ /opt/TPTP-v7.5.0/TPTP2X/tptp2X_install
...対話的にインストールの方法に答える

--------------------------------------------------------------------
                tptp2X installation complete
--------------------------------------------------------------------

その後は TPTP and TSTP Quick Guide を読んでいく

TPTP

解説をつけながら読み進める

TH1: The TPTP Typed Higher-Order Formwith Rank-1 Polymorphism のPDFによると

• TPTPでは
  • CNF(=first-order clause normal form)のみがサポートされていた
    • CNFとは一階述語論理を拡張した言語である。by Clause Normal Form
    • 一階述語論理は命題論理を拡張したものである。

その後数年して以下がサポートされるようになった

• FOF(=full first-order form)
• TF0(=monomorphic typed first-order form)
• TF1(=rank-1 polymorphic typed first-order form)
• TH0(=monomorphic typed higher-order form)

上記の一覧（よくわからない抽象的な図表入り）は Menu of Reliability から見れる。が、それを見るよりは TH1: The TPTP Typed Higher-Order Formwith Rank-1 Polymorphism のPDFを見たほうがまだわかりそう。

上記の詳細を調べようと思ったが、論文にアクセスできないので見れなかった。とりあえず略語が何かわかったということで。

...

• 問題を解くためのTPTP形式
  • 問題(Problem)は数式のリストです。
  • THF(=typed higher-order form)、TFF(=typed first-order form)、およびFOF(=(full) first-order form)では、式は通常、任意の数の公理と1つの予想です。
  • CNF(=clause normal form)では、公式は通常、任意の数の公理と1つ以上の否定された予想です。

• TPTPには数学のドメイン（分野）がIDとして英語の頭文字で定義されている
  • ドメインの一覧は: The TPTP Domain Structure
  • なので３文字の英語が出てきたらTPTPで定義された数学のドメインと考えていい

• TPTPの問題ファイルを作成するには
  • ↑ここ一番わかりやすいと思うので頑張って訳す

Propositional Logic (PRP)

• Propositional Logic (命題論理)

First-order Logic (FOF)

• First-order Logic (一階述語論理)

Typed First-order Logic (TFF)

• Typed First-order Logic (型付き一階述語論理)

Typed Higher-order Logic (THF)

• Typed Higher-order Logic(型付き高階述語論理)