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…

「それ以降は投げない」という条件のみ，標本点の生成時に適用します． 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…

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

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

これも「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,…

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

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

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

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

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…

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) …

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

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…

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…

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). (…

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…

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

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…

一般に環では|-∀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…

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

昨日のシステムでは出力が長いので，古典論理に絞り，二重否定除去のルール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に，有理数体上の有理式を項とし，＝，＜，＞，≦，≧を2項述語記号とする（量化記号のない）論理式を有理整数環上の多項式を項とする論理式に変換するコマンドtoimplxを実装してみました． 論理記号は，否定negx，選言orx，連…

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

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

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

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

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