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((negx(aa))orx(negx(bb))); aa eqx bb:=((aa)andx(bb))orx((negx(bb))andx(negx(aa))); */ aa replx bb:=(bb)implx(aa); aa andx bb:=negx((aa)implx(negx(bb))); aa eqx bb:=((aa)implx(bb))andx((aa)replx(bb)); defrule(negneg,((aa)implx(0=1))implx(0=1),(aa)); defrule(sf1,aa>=bb,bb<=aa); defrule(sf2,aa>bb,bb<aa); defrule(fr1,aa=bb,xthru(aa)=xthru(bb)); defrule(fr2,aa<bb,xthru(aa)<xthru(bb)); defrule(fr3,aa<=bb,xthru(aa)<=xthru(bb)); matchdeclare(rr,lambda([x],is(denom(x)#1))); defrule(cd1,rr=cc,(num(rr)=cc*denom(rr)) andx (negx(denom(rr)=0))); defrule(cd2,cc=rr,(num(rr)=cc*denom(rr)) andx (negx(denom(rr)=0))); defrule(cd3,cc<=rr, ( (0<denom(rr)) andx (cc*denom(rr)<=num(rr)) ) orx ( (denom(rr)<0) andx (num(rr)<=cc*denom(rr)) ) ); defrule(cd4,cc<rr, ( (0<denom(rr)) andx (cc*denom(rr)<num(rr)) ) orx ( (denom(rr)<0) andx (num(rr)<cc*denom(rr)) ) ); defrule(cd5,rr<=cc, ( (denom(rr)<0) andx (cc*denom(rr)<=num(rr)) ) orx ( (0<denom(rr)) andx (num(rr)<=cc*denom(rr)) ) ); defrule(cd6,rr<cc, ( (denom(rr)<0) andx (cc*denom(rr)<num(rr)) ) orx ( (0<denom(rr)) andx (num(rr)<cc*denom(rr)) ) ); toimplx1(x):=applyb1(x,negneg,sf1,sf2,fr1,fr2,fr3,cd1,cd2,cd3,cd4,cd5,cd6); toimplx(x):=toimplx1(toimplx1(x));
入出力例
toimplx(y=1/x); (%o22) (1=x*y) implx (x=0) implx (0=1) toimplx(negx(y=1/x)); (%o23) (1=x*y) implx (x=0) toimplx((0<=1/x)eqx(a<x)); (%o24) (0<x) implx ((0<=1) implx (0=1)) implx ((x<0) implx ((1<=0) implx (0=1)) implx (0=1)) implx ((a<x) implx (0=1)) implx ((a<x) implx (0=1) implx ((0<x) implx ((0<=1) implx (0=1)) implx ((x<0) implx ((1<=0) implx (0=1)) implx (0=1))) implx (0=1)) toimplx(((0<x) andx (0<y)) implx (x/y+y/x>=c)); (%o25) (0<x) implx ((0<y) implx (0=1)) implx (0=1) implx ((0<x*y) implx ((c*x*y<=y^2+x^2) implx (0=1)) implx ((x*y<0) implx ((y^2+x^2<=c*x*y) implx (0=1)) implx (0=1)))