JAPE

*JAPE JAPE(J∀P∃)はユーザーが論理体系,理論をコード化し,証明図(Fitch diagrams,Gentzen trees)やcounter model(Kripke diagrams)を簡単なマウス操作により作成できるproof calculatorです. // - Japeカーネルにコード化の仕様(テキストファイ…

qepmax

以前,mathlibre の wiki に書いたものです(wiki はサーバーのトラブルで最近の記事が消えています) *maxima からの利用 「qepmax」パッケージをロードすると,maxima 上から QEPCAD B が利用できます. 論理記号 %implies %replies %eq %or %and %neg A E…

The Flyspeck Project

final result です. # tame_nonlinear_imp_kepler_conjecture;; val it : thm = |- import_tame_classification /\ the_nonlinear_inequalities ==> the_kepler_conjecture # SIMP_RULE [the_kepler_conjecture_def; import_tame_classification; the_nonli…

2011年一橋大第5問

「それ以降は投げない」という条件のみ,標本点の生成時に適用します. FindSequenceFunction[Function[n, S = Tuples[{a2, a3, a6, b2, b3, b6}, n] /. {{x___, a6, ___} -> {x, a6}, {x___, b6, ___} -> {x, b6}} // DeleteDuplicates; F1 = Select[S, Len…

2014年東大前期文科第2問

RSolveではなく...,標本点を長さnのリストとして,標本空間S,好ましい事象F,確率測度を導入し,n=1,2,3,4でFの像(確率)を FindSequenceFunction に渡します. FindSequenceFunction[ Function[n, S = Tuples[{w, r}, {n}]; F = Select[S, Last@# ===…

1988年東大前期理科第2問

これも如何に変数の個数と次数を小さくするかですが,... ・射影は並進不変である ・平面αのみを動かせばよい ・影Sの内点は四面体の丁度2個の境界点(表面の点)の像となる(つまり各面の影の面積の和の半分がSの面積) ・各面の法線ベクトルは四面体の…

1988年東大前期理科第6問

これも「Vがその四面体の体積となる」という論理式を,mmaに RS = Reduce[ Exists[{a, b, c}, And[0 <= a, 0 <= b, 0 <= c, 0 <= S == a*b*c/(4*R), (a/(2*R))^2 + ((b^2 + c^2 - a^2)/(2*b*c))^2 == 1]], Reals] Reduce[Exists[{S, R, d, x, y, z}, And[RS,…

QEPCAD B の Xk の利用例

1988年東大前期理科第3問 mmaだと https://kaigi.org/jsai/webprogram/2014/paper-768.html のような感じでしょうが,qepmaxだと となります.

HOL(y) Hammer

リモートが動かなくなったと思っていたら,オンラインのインターフェイスが公開されていました.例えば,... g `!n. &1 + &n <= &2 pow n` ;; の証明スクリプト.人(私)が書くと e( INDUCT_TAC THEN REWRITE_TAC [REAL;pow] THEN ASM_ARITH_TAC );; と…

Theorema 2.0

http://www.risc.jku.at/research/theorema/software/ https://github.com/windsteiger/Theorema http://www.risc.jku.at/research/theorema/software/documentation/tutorial/FirstTour.html

Mathematica 10

http://www.wolfram.com/mathematica/new-in-10/

Wellfounded induction(2)

http://d.hatena.ne.jp/ehito/20111119/1321692292 のPVS版です. lem00:lemma FORALL (p: pred [nat]): (FORALL (n: nat): (FORALL (k: nat): k < n IMPLIES p(k)) IMPLIES p(n)) IMPLIES (FORALL (n: nat): p(n)) %|- lem00 : PROOF %|- (then (skeep*) (c…

HOL Light vs PVS (2)

http://d.hatena.ne.jp/ehito/20130816/1376622603 の続編です. 前回は n≦n*n を sub goal としましたが,今回は結論に含め,帰納法の仮定を強くしました. g `!n. &0 <= &n * (&n - &1) * (&n - &2) /\ &0 <= &n * (&n - &1) /\ &1 + &n + &n * (&n - &1) …

Formally Verified Mathematics

http://cacm.acm.org/magazines/2014/4/173219-formally-verified-mathematics/fulltext

Proof by pointing

http://logitext.mit.edu/logitext.fcgi/main https://github.com/ezyang/logitext/blob/master/doc/report.pdf

含意と特称

以前にも書いた排中律ネタですが,今回は連言から存在量化を纏める形のものです. g `!p:A->bool. !q:bool. (?x. p x ==> q) ==> (?y. q ==> p y) ==> (?z. p z <=> q)`;; e( REPEAT STRIP_TAC );; e( DISJ_CASES_TAC (SPEC `q:bool` EXCLUDED_MIDDLE) );; e…

A survey of automated theorem proving

https://www.youtube.com/watch?v=Nydg-N83VYc https://www.youtube.com/watch?v=iPFJY0aW4E4 https://www.youtube.com/watch?v=ZdJ0-V77f_0 https://www.youtube.com/watch?v=g3EQKBMq5h0 http://logic.pdmi.ras.ru/csclub/sites/default/files/slides/2013…

qepmax

maximaをAndroidに移植された本田康晃(https://sites.google.com/site/maximaonandroid/)さんが,maximaからQEPCAD Bへのインターフェイスqepmax(https://github.com/YasuakiHonda/qepmax)を公開しておられます.このqepmaxは,オリジナルのQEPCAD Bの拡…

不等式

# prove( `!a b c A B C. &0 < a /\ a <= b /\ b <= c /\ c < a + b /\ &0 < A /\ A <= B /\ B <= C /\ A + B + C = &180 ==> &60 <= (a * A + b * B + c * C) / (a + b + c) /\ (a * A + b * B + c * C) / (a + b + c) < &90`, REPEAT STRIP_TAC THEN REWRI…

体の公理

乗法逆元の存在の公理におけるx=0の違和感?をなくした公理系を考えました.そのココロは (x=0|x*y=1)->(x*(x*y)=x)はOK,整域なら逆もOK です.Axioms: (all x all y all z (x + y) + z = x + (y + z)). (all x all y x + y = y + x). (all x x + 0 = x). (…

maximaのロジックシステム(6)

http://d.hatena.ne.jp/ehito/20140506/1399341060 で述べた「分母≠0の付帯」という慣習を実装したCASはあるのでしょうか? 例えば,Mathematicaは In[1]:= Reduce[ForAll[{x, y, z}, y == z/x, Not[x == 0]], Reals] Out[1]= True In[2]:= Reduce[ForAll[{x…

maximaのロジックシステム(5)

また経緯があり,ロジカルな処理は(あまり)行わず,有理式の(それなりに)正確な簡約のみを行うratsimpx2を書きました. 論理結合子 %implies,%or,%and は既にあるものとして,%neg,%replies,%eq を新規に導入しますが,出力に現れるのは先の3つのみ…

maximaのロジックシステム(4)

QEPCAD BのF,G,C,X k(http://d.hatena.ne.jp/ehito/20110523/1306130261)に対応する関数nf,fn,cs,ex0,ex1,ex2,ex3,ex4を追加しました. cs,ex*の引数は論理式ではなくラムダ関数です. 実用に供するには,最後のtoimplxの定義のtopnfxの直前で,ALPHA CONV…

0の逆元

一般に環では|-∀y(0*y=0)なので,|-∃y(0*y=1)となる環は零環(0のみからなる環)に限る. これを避けて一般に体では¬(0=1)も公理とし,∀x∃y(x=0∨x*y=1)を公理にする. 対応する選択関数の一つを1/で表すと,この公理は∀x(x=0∨x*(1/x)=1)と表せる. とくに,1…

maximaのロジックシステム(3)

量化記号all,exも使えるようにしました.すなわち,all(束縛変数,論理式)およびex(束縛変数,論理式)は論理式であり,all,exから始まる論理式はこの形に限ります. ただし,束縛変数は入力時に区別する必要があります(勝手にalpha-convしません.したがって…

maximaのロジックシステム(2)

昨日のシステムでは出力が長いので,古典論理に絞り,二重否定除去のルールnegnegを追加します. map(infix,[implx,orx,andx,eqx,replx]); matchdeclare([aa,bb,cc],true); negx(aa):=(aa)implx(0=1); aa orx bb:=(negx(aa))implx(bb); /* aa andx bb:=negx(…

maximaのロジックシステム(1)

ちょっとした経緯があり,maximaに,有理数体上の有理式を項とし,=,<,>,≦,≧を2項述語記号とする(量化記号のない)論理式を有理整数環上の多項式を項とする論理式に変換するコマンドtoimplxを実装してみました. 論理記号は,否定negx,選言orx,連…

今年の京都大学の理系数学入試問題

季節ネタということで,人間がコードを書いた場合の解答例を記していきます. 問題はこんな感じ.http://mainichi.jp/graph/edu/daigakubetsu/kyotosugaku2/001.html[1]設定通りに点,ベクトルを導入,p,q,rの満たす条件をpa1,pa2,pa3のRuleで表したもの…

自動解答系の作り方(20)

折角なので自動解答システムに適した「正方形」の定義の例を述べておきます. まず,座標幾何の言葉を用いることに異論はないと思います. 次に正方形の実体?ですが,ここでは「頂点の列」を正方形とします. で,その特徴付けですが,不慣れな受験生のよう…

自動解答系の作り方(19)

昨日の東ロボくんの番組に出てきた正方形の面積の話. 「正方形」及び,その「辺」,「面積」をどのように定義して上での処理か判らないので何とも評価できませんが,画面から察するに方針としては「1辺の長さが2であり,面積がxgen3である正方形が存在す…

自動解答系の作り方(18)

今回は関数のグラフに限らず,一般の「曲線に囲まれた図形の面積」を定義し,それを求めるMathematicaのコマンドコードを公開します. R^2の部分集合からRへの関数族 {f_{k}}_{k∈{1,...,n}} に対して,∃k.( f_{k}(x,y) = 0 ∧ k∈{1,...,n} ) を満さない(つま…

自動解答系の作り方(17)

センターに限らず「関数のグラフで囲まれた図形」の面積は入試における頻出事項ですが,「その図形」の定義は数学にはなく,出題者と解答者との曖昧さのシンパシーによって維持されたもので,複数の解釈ができる問題も散見されます. ということで,今回のシ…

自動解答系の作り方(16)

多項式関数の微積分に対する方針は,2次関数と同じく,接線の方程式,極値やそれに対応する定義域内の要素,関数のグラフなどで囲まれた集合の面積を出力する関数を準備,適用するのみで,数学としての面白みにやや欠ける為,後回しにしていたのですが,少…

自動解答系の作り方(15)

第4問は問題の読み取りが不可能なのでどうしようもありません.なお,本問は数学としてはアイゼンシュタインの整数というかベクトル値の確率変数が導入された確率空間の話なので,仕組みはサイコロの目の数の和などと同じですから,人間が機械的(つまり組…

自動解答系の作り方(14)

処理における留意点などを書いていきます.第3問三角比に対してすぐ思い付くのは,教科書通り(ア)余弦・正弦定理,角の2等分線や円周角の性質を適用する方法と(イ)座標による方法でしょう.(ア)は高速で,序盤の設問のような単純な場合には有効です…

自動解答系の作り方(13)

処理における留意点などを書いていきます.第2問これは2012年度の類題なので,頂点の座標,平行移動,最大・最小値及び対応する定義域内の元,x軸との共有点の座標の条件は既に組んでいた関数が適用され,y軸切片のマッチングパターンを追加すれば数学の部…

自動解答系の作り方(12)

処理における留意点などを書いていきます.第1問〔2〕集合のルーチンは用意していませんでしたので新規に組みました.アルゴリズムはMathematicaらしいもので約0.06秒で結果に至ります.それはいいのですが,問題文の「空集合であるものは〜である」「成り…

自動解答系の作り方(11)

処理における留意点などを書いていきます.第1問〔1〕これは既存のルーチンのみで通りました...では記事にならないので,少し細かなことを書きます.まず「A=Bとおく」の評価ですが,今回を含めセンター試験問題では多くの場合,Aが新たに導入されるも…

自動解答系の作り方(10)

前回に続いて,数学1A第1〜3問のデモ動画です. [

自動解答系の作り方(9)

2014年度センター試験数学1A第1問〔1〕 〔1〕$a=\frac{1+\sqrt{3}}{1+\sqrt{2}}$,$b=\frac{1-\sqrt{3}}{1-\sqrt{2}}$とおく. (1)$a b=ans[1]$ $a+b=ans[2] ({ans[3] ans[4]} +\sqrt{ans[5]})$ $a^2+b^2=ans[6] (ans[7] -\sqrt{ans[8]})$ である. (2…

自動解答系の作り方(8)

空欄を多く含む論理式の扱いはそれなりに工夫を要します.実際,空欄の個数が5を超える場合,軽い処理のループでもかなり時間が掛かります. 幾つかのケースでは式を分割することもできるのですが,例えば,2009年度本試験数IIB第3問の最後に現れる $$U_{n…

自動解答系の作り方(7)

今回のシステムでは,問題文を先頭から末尾に向けて走査し対象を定義していくのですが,そのままでは定義の上書きが起こることがあります.次は前回の2013年数学ⅡB第4問の問題文の一部です. また,点$A$を通り直線$BD$に垂直な直線と直線$OC$の交点を$E$…

自動解答系の作り方(6)

解答コマンドの生成には,大きく分けて 【1】問題文の分解と項や論理式の抽出 【2】Mathematicaコードへの変換 【3】コマンドへの埋め込みと合成のステップがあります. 【1】は$で挟まれたLaTeXコード(及びそれに準じた「$a$は正の数」など)を述語の…

自動解答系の作り方(5)

センター試験の ・ベクトルの問題 ・三角比の問題に対応しました.入力と出力の例を挙げます.2013数学ⅡB第4問 $OA=5$,$OC=4$,$\angle{AOC}=\theta$である平行四辺形$OABC$において,線分$OA$を$3:2$に内分する点を$D$とする. また,点$A$を通り直線$BD…

自動解答系の作り方(4)

センター試験の ・2次関数の問題 ・(帰納的に構成された)数列の問題に対応しました.入力と出力の例を挙げます.2012数学ⅠA第2問 $a,\ b$を定数として2次関数 $$y=-x^2+(2a+4)x+b\ \cdots\ \textcircled{1}$$ について考える. 関数$\textcircled{1}$の…

自動解答系の作り方(3)

数学のセンター試験はいわゆる空所補充,つまり,問題文自体が数学的な主張になっているものが殆どです.また,一部の並び順を除けは正解は一意的です.従って,その主張をMathematicaの流儀による論理式に書き換えさえすれば,後はループを用いて空欄に選択…

自動解答系の作り方(2)

センター試験の自動解答へのアプローチには(A)二次試験と同じく自前で得た結果を設問の空欄に当てはめる(B)設問の空欄に全ての選択肢を当てはめたものから正しいものを見出すという2つが考えられます. (A)で不都合なのは途中経過,従って誘導部分の…

リビジョンアップ

Isabelle2013-2 が公開されました.http://www.cl.cam.ac.uk/research/hvg/Isabelle/

自動解答系の作り方(1)

突然(でもない?)ですが,日本語混じりの LaTeX の問題文を入力とする自動解答システムを試作しました.扱い易い問題ならそれなりに処理できるようになりましたので,これについて書いていこうと思います. 自動解答といっても QE を含めた数式処理は Math…

東ロボくんのこと(15)

第3問です.http://www.yozemi.ac.jp/nyushi/sokuho/recent/tokyo/zenki/ これも最小値の定義を適用し,minが設問の最小値に等しいという式を Mathematica に処理させるなら Reduce[Exists[{x,y},x^2 + y^2 <= 25&&2x + y<=5 , min== x^2 + y^2 - 2a x - 2b…