以前にも述べましたが，変数の個数を低減させた必要条件を付加する ncond は強力で，nnss，nnsolvexx の求解能力はこの関数によるヒントの賜物とも言えます． (%i98) f:(a^2+b^2+c^2<=3)%and(a*b*c>=1)$ Evaluation took 0.0100 seconds (0.0200 elapsed) us…

次の不等式を簡約します． (%i90) f:x^3+y^3+z^3>=3*x*y*z; Evaluation took 0.0000 seconds (0.0000 elapsed) using 1.859 KB. (%o90) z^3+y^3+x^3 >= 3*x*y*z まずは，qepmax から．．．． (%i91) qe([],f); Evaluation took 0.0800 seconds (0.2700 elaps…

次の不等式を簡約します． (%i86) f:(x^2-1)*(x^2-4)*(x^2-9)<0; Evaluation took 0.0000 seconds (0.0000 elapsed) using 1.344 KB. (%o86) (x^2-9)*(x^2-4)*(x^2-1) < 0 まずは，qepmax + nns です．悪くはありませんが，ちょっと解り難いですね． (%i87) …

式の簡約は，まず選言形に直し，得られた連言項毎に処理するのが基本です．よって結果は (%i70) qe([],(a^2=1)%and(b^2=1)); Evaluation took 0.3400 seconds (0.5200 elapsed) using 12.210 MB. (%o70) (a-1 <= 0) %and (a+1 >= 0) %and (((a-1 = 0) %and (…

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

各言語の任意の論理式は，証明論においては，証明系で証明できる式，すなわち，定理式か否かに，モデル論においては，任意の構造，任意の変数への個体割り当てに対して真となる式，すなわち，恒真式か否かに，それぞれ分類されますが，その分類が同じ結果と…

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

古典的（？）な一階の古典論理の意味論では，ドメイン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 とすると，emacsが起動し M-x nf でNew file name:と尋ねられ，例えばdemoe20160519と適当に入力すれば，demo20160519.pvsが demo20160519 % [ parameters ] : THEORY BEGIN % ASSUMING % assuming declarations % END…

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

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 …