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，連…