maximaのロジックシステム（２）

　昨日のシステムでは出力が長いので，古典論理に絞り，二重否定除去のルール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)))