FreeStyleWiki

TPTP

このエントリーをはてなブックマークに追加

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

TPTP

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

  事始め

The TPTP World Tutorial を読んでいく

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

  • 世界の問題を論理に変換する
    • 公理(Axioms)はあなたが世界について知っていることを説明します
    • 予想(Conjecture)は何を解決する必要があるかを説明します
  • 論理解決策を得るために自動推論を使用する
    • 自動証明器(theorem prover)は証明を見つける
    • モデルファインダー有限カウンターモデル
    • モデルファインダーは公理が一貫していることを確認します
  • 論理解決策を世界に翻訳する
    • 予想の証明は解決策を説明します
    • カウンターモデルは、解決策がない理由の例です
筆者注
theorem prover(自動証明器)と呼ばれるものは世界にいくつもあるようだ SystemOnTPTP の画面左側にあるもので、GitHubへのリンクがあったりするが、それらがすべて自動証明器。 TPTPはそのファイルフォーマットを定めていると言える

  TPTPのインストール

Getting and Using the TPTP

// 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によると

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

    • 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として英語の頭文字で定義されている

Propositional Logic (PRP)

First-order Logic (FOF)

Typed First-order Logic (TFF)

Typed Higher-order Logic (THF)