nns シリーズ

maxima 上の QE パッケージである qepmax の周辺関数を幾つか公開します.各関数の入力と出力とは等価な式です.・dnf,cnf 選言,連言形に変換 ・ncond 変数の個数の低減(大規模な式も扱えるように map から for ループに変更しました) ・nns,nnscan,nnsca…

LK の健全性の証明

各シグネチャーから得られる任意の論理式は,証明論においては,証明系で証明できる式,すなわち,定理式か否かに,モデル論においては,任意の構造,任意の変数への個体割り当てに対して真となる式,すなわち,恒真式か否かに,それぞれ分類されますが,そ…

「開いた式」

「開いた式」とは「変数の自由出現(あるいは自由変数)を含む論理式」のことで,その真理値の定め方には幾つかの立場があります.言語,構造を固定した上で,伝統的(?)なのは,変数への個体割り当てを用いて立場1 割り当て毎に真偽を与える立場2 割り…

Empty domain

古典的(?)な一階の古典論理の意味論では,ドメインAは空でないとされ,その理由として,Aが空では,∀x.p(x),つまり「任意のxについて,x∈Aならばp(x)」が真,∃x.p(x)つまり「あるxについて,x∈Aかつp(x)」が偽,したがって,定理式 ∀x.p(x)→∃x.p(x) が偽…

PVSの使い方

今更ですが,使い方です.端末から pvs とすると,emacsが起動し M-x nf でNew file name:と尋ねられ,例えばdemoe20160519と適当に入力すれば,demo20160519.pvsが demo20160519 % [ parameters ] : THEORY BEGIN % ASSUMING % assuming declarations % END…

skeep

PVSのskeepコマンドは,本来は x!1 などのように新規に導入すべきスコーレム定数を,衝突がない限り束縛されていた変数と同じ名前で導入してくれます. f1 : |------- {1} (EXISTS (x: A): (p(x))) AND (EXISTS (x: A): (q(x))) => (EXISTS (x: A): (p(x) AN…

HOL Light vs PVS (3)

g `!n. 8 <= n ==> (?x y. n = 3 * x + 5 * y)` ;; e( INDUCT_TAC );; e( ARITH_TAC );; e( REWRITE_TAC [LE] THEN REPEAT STRIP_TAC );; e( EXISTS_TAC `1` THEN EXISTS_TAC `1` THEN ASM_ARITH_TAC );; e( FIRST_X_ASSUM (fun t -> FIRST_ASSUM (MP_TAC o …

計算機は囁く

Mathematica は当然 In[5]:= Reduce[Exists[x, 0 <= x <= 1 && y == x^2 - 2 a x], Reals] Out[5]= (a <= 0 && 0 <= y <= 1 - 2 a) || (0 < a <= 1/2 && -a^2 <= y <= 1 - 2 a) || (1/2 < a <= 1 && -a^2 <= y <= 0) || (a > 1 && 1 - 2 a <= y <= 0) と答え…

set_goal

set_goal([`&0 < b pow 2 - &4 * a * c`],`?x. a * x pow 2 + b * x + c = &0`);; e(ASM_CASES_TAC `a = &0`);; e(ASM_CASES_TAC `b = &0`);; e( X_GET_TAC 0 );; e( ASM_SIMP_TAC [] );; e( ARITH_TAC );; e( EXISTS_TAC `-- c / b` );; e( ASM_REAL_FIELD_…

maxima 5.37.0, wxMaxima 15.08.0

公開されました. Maxima -- GPL CAS based on DOE-MACSYMA - Browse Files at SourceForge.net wxMaxima - Browse /wxMaxima at SourceForge.net

冪乗と階乗

g(`!n. 3 < n ==> 2 EXP n < FACT n`);; e(INDUCT_TAC);; e(ARITH_TAC);; e(SIMP_TAC[LT;EXP;FACT]);; e(STRIP_TAC);; e(POP_ASSUM (SUBST1_TAC o GSYM) THEN ARITH_TAC);; e(MATCH_MP_TAC LESS_MULT);; e(ASM_ARITH_TAC);; prove (`!n. 3 < n ==> 2 EXP n <…

fourier_elim を懐柔する(その2)

前回の qfq では,例えば (%i1) f:abs(x-a)=abs(x-b)+c; (%o1) abs(x - a) = abs(x - b) + c (%i2) qfq(f); (%o2) ((0 < c) %and (a = b - c) %and (x = b)) %or ((0 < c) %and (b = a - c) %and (x = a - c)) %or ((a = b) %and (c = 0) %and (x = b)) %or …

fourier_elim を懐柔する

abs や max,min も気軽に使えるよう,fourier_elim を内蔵した fqe を作りました. f2q(f):=subst([universalset=true,emptyset=false,"or"="%or","["="%and"],f)$ qfq(f):=block([g], if op(f)="%and" then (g:args(f),f2q(fourier_elim(g,listofvars(g)))…

動かない式を動かす(nnsolve その4)

まず,次をご覧ください. (%i1) f:((x-1/x)^2+(y^2-4*y+5)^3+(z+1)^2/z^4<=1)%and(x<0); 2 (z + 1) 2 3 1 2 (%o1) (x < 0) %and (-------- + (y - 4 y + 5) + (x - -) <= 1) 4 x z 人間が見るとバレバレですが,ストレートな qepmax では (%i2) qe([],f); 2…

solve とともに(nnsolve その3)

solve は非常に強力な関数で (%i1) solve(x=y,[x,y]); (%o1) [[x = %r1, y = %r1]] と解いてくれます(笑).これを抑えるには (%i2) solve(x=y,[x,y]),linsolve_params:false; (%o2) [[x = y]] とすればよいのですが,次数が上がると,聞く耳を持たないご様…

dnf と cnf(nnsolve その2)

選言標準形,連言標準形は代数で言えば,それぞれ展開,因数分解に当たる基本的なものであり,前者は所謂(排他的とは限らない)場合分けなので,方程式系の解の構成には欠かせません.その実装は簡単で,例えば,A ∧ (B ∨ C) を (A ∧ B) ∨ (A ∧ C) に可能な…

nnsolve その1

原理は単純で,入力 f を選言標準形 ∨_k f_k に直し,f_k を方程式系部分 p_k と,不等式・非等式系部分 q_k との連言 p_k ∧ q_k に分解,p_k を maxima の solve で処理した結果 r_k を用いて,∨_k (r_k ∧ q_k) を出力とするものです.実装において問題とな…

能動的な簡約

QEPCAD B,従って,qepmax では (%i1) qe([[A,x]],(x=1)%eq(x^2+a*x+b=0)); 2 (%o1) (a - 4 b = 0) %and (b + a + 1 = 0) (%i2) qe([[A,x]],(x^2+x=1)%implies(x^2+a*x=b^2)); 4 2 2 2 (%o2) (a - 1 = 0) %and (b + a b - 3 b - a + a + 1 = 0) のように簡約…

nnscan

nns は最も外にある %and または %or に作用するのみなので (%i1) nns(((x>=0)%and(x=0))%or((x>=1)%and(x=1))); (%o1) ((x = 0) %and (x >= 0)) %or ((x = 1) %and (x >= 1)) (%i2) nns((((x>=0)%and(x=0))%or((x>=1)%and(x=1)))%and((y>=0)%and(y=0))); (%…

高速化

アルゴリズムを「簡約」し,コストを半減させました. nns(f):= block([cl,L,fk],cl(f,g):=length(f)<=length(g), L:sort(rest(full_listify(powerset(setify(args(f))))),cl), if op(f)="%and" then for k:1 thru length(L) do (fk:substpart("%and",part(L…

clisp,sbcl,cmucl

nnsの原理は冪集合によるものなので,式が少し長くなるとそれなりに時間が掛かります.ということで,Lispを替えて実行してみると... のように,速度,メモリのバランスはやはり cmucl が良さそうです.

出力の簡約

QEPCAD B,従って,qepmax では (%i1) qe([],x^2=1); (%o1) (x - 1 <= 0) %and (x + 1 >= 0) %and ((x - 1 = 0) %or (x + 1 = 0)) (%i2) qe([[X2,x]],x^2+a*x+1=0); (%o2) (a - 2 # 0) %and (a + 2 # 0) %and ((a - 2 > 0) %or (a + 2 < 0)) のように簡約が…

インストールスクリプト

Redlog,REDUCE のコードが更新されました.最新版の maxima(5.36.1),wxmaxima(15.04.0)も併せて書いておきます. mkdir ~/CAS (* WxWidget http://codelite.org/LiteEditor/WxWidgets30Binaries#toc2 *) (* resuce csl 及び wxmaxima には必要 *) sudo…

qepmax

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

JAPE

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

選言から連言へ

ちょっとした経緯があり,NK,LKにおけるド・モルガン則の証明の作成手順を述べます.ド・モルガン則は,¬(〇*□)⇔(●・■)の形の定理(〇は●の否定,■は■の否定,*,・の一方は,∨他方は∧)であり,証明は¬(〇*□)⊢(●・■)と(●・■)⊢¬(〇*□…

選言から連言へ

ちょっとした経緯があり,NK,LKにおけるド・モルガン則の証明の作成手順を述べます.ド・モルガン則は,¬(〇*□)⇔(●・■)の形の定理(〇は●の否定,■は■の否定,*,・の一方は,∨他方は∧)であり,証明は¬(〇*□)⊢(●・■)と(●・■)⊢¬(〇*□)…

Algorithms for Trigonometric Curves (Simplifcation,Implicitization,Parameterization)

H.HONG,J.SCHICHO.Jurnal of Symbolic Computation 26(1998),279-300. (* 次数 *) TrigDegree[ft_, t_] := Exponent[TrigToExp@ft, Exp[I t]]; (* 主係数 *) TrigLeadingCoefficient[ft_, t_] := Coefficient[TrigReduce@ft, Through[{Cos, Sin}[TrigDegree[…

Algorithms for Trigonometric Curves

TrigDegree[ft_, t_] := Exponent[TrigToExp@ft, Exp[I t]]; TrigLeadingCoefficient[ft_, t_] := Coefficient[TrigReduce@ft, Through[{Cos, Sin}[TrigDegree[ft, t] t]]]; TrigQuotientRemainder0[ft_, gt_, t_] := Block[{X = TrigLeadingCoefficient[ft,…

JAPE

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