MetiTarski
の編集
http://list.mathlibre.org/wiki/?MetiTarski
[
トップ
] [
編集
|
差分
|
バックアップ
|
添付
|
リロード
] [
新規
|
一覧
|
検索
|
最終更新
|
ヘルプ
]
-- 雛形とするページ --
(no template pages)
*MetiTarski 2.3 [#t2e2cb58] MetiTarski is an automatic theorem prover based on a combination of resolution and a decision procedure for the theory of real closed fields. It is designed to prove theorems involving real-valued special functions such as log, exp, sin, cos and sqrt. In particular, it is designed to prove universally quantified inequalities involving such functions. This problem is undecidable, so MetiTarski is necessarily incomplete. Nevertheless, MetiTarski is remarkably powerful. 不等式評価を公理に加えることにより初等超越関数まで扱うプルーバーです. *インストール例 [#vca880ef] - http://d.hatena.ne.jp/ehito/20130807/1375832972 *使用例 [#ec0d08f4] echo "fof(test,conjecture,! [X]:(0<=X => 1+sin(X)<=exp(X)))." | metit --autoInclude - *リンク [#j5d9cbf2] - http://www.cl.cam.ac.uk/~lp15/papers/Arith/ - http://www.cl.cam.ac.uk/~lp15/papers/Arith/ITP%202012%20presentation.pdf - http://www.cl.cam.ac.uk/~lp15/papers/Arith/MetiTarski-jar.pdf
タイムスタンプを変更しない
*MetiTarski 2.3 [#t2e2cb58] MetiTarski is an automatic theorem prover based on a combination of resolution and a decision procedure for the theory of real closed fields. It is designed to prove theorems involving real-valued special functions such as log, exp, sin, cos and sqrt. In particular, it is designed to prove universally quantified inequalities involving such functions. This problem is undecidable, so MetiTarski is necessarily incomplete. Nevertheless, MetiTarski is remarkably powerful. 不等式評価を公理に加えることにより初等超越関数まで扱うプルーバーです. *インストール例 [#vca880ef] - http://d.hatena.ne.jp/ehito/20130807/1375832972 *使用例 [#ec0d08f4] echo "fof(test,conjecture,! [X]:(0<=X => 1+sin(X)<=exp(X)))." | metit --autoInclude - *リンク [#j5d9cbf2] - http://www.cl.cam.ac.uk/~lp15/papers/Arith/ - http://www.cl.cam.ac.uk/~lp15/papers/Arith/ITP%202012%20presentation.pdf - http://www.cl.cam.ac.uk/~lp15/papers/Arith/MetiTarski-jar.pdf
テキスト整形のルールを表示する