TPTP
TPTPはPrologで書かれた自動定理証明のためのライブラリ。
追記: 自動定理証明や単純な代数計算に関しては、もっと新しいものや手軽に使えるSageMathのようなものを使った方がいい気がする
事始め
- Prologのインストール Prolog入門 はここで
The TPTP World Tutorial を読んでいく
What is Automated Reasoning?(自動推論とは何ですか?)
- 世界の問題を論理に変換する
- 公理(Axioms)はあなたが世界について知っていることを説明します
- 予想(Conjecture)は何を解決する必要があるかを説明します
- 論理解決策を得るために自動推論を使用する
- 自動証明器(theorem prover)は証明を見つける
- モデルファインダー有限カウンターモデル
- モデルファインダーは公理が一貫していることを確認します
- 論理解決策を世界に翻訳する
- 予想の証明は解決策を説明します
- カウンターモデルは、解決策がない理由の例です
- 筆者注
- theorem prover(自動証明器)と呼ばれるものは世界にいくつもあるようだ SystemOnTPTP の画面左側にあるもので、GitHubへのリンクがあったりするが、それらがすべて自動証明器。 TPTPはそのファイルフォーマットを定めていると言える
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
- 一階述語論理は命題論理を拡張したものである。
- CNF(=first-order 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
- なので3文字の英語が出てきたらTPTPで定義された数学のドメインと考えていい
- TPTPの問題ファイルを作成するには
- ↑ここ一番わかりやすいと思うので頑張って訳す