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

　ちょっとした経緯があり，maximaに，有理数体上の有理式を項とし，＝，＜，＞，≦，≧を2項述語記号とする（量化記号のない）論理式を有理整数環上の多項式を項とする論理式に変換するコマンドtoimplxを実装してみました．

　論理記号は，否定negx，選言orx，連言andx，等価eqxの全てを含意implxに帰着させるスタイルです．

infix(implx);
infix(orx);
infix(andx);
infix(eqx);
matchdeclare(aa,true,bb,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)));

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)),cc,true);
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,sf1,sf2,fr1,fr2,fr3,cd1,cd2,cd3,cd4,cd5,cd6);
toimplx(x):=toimplx1(toimplx1(x));

　結合の強さはデフォルトのままなので，項は丸カッコで挟む必要があります．また，非等号＃は用いず，negxで等式を否定して下さい．

　入出力例

toimplx(y=1/x);
(%o51) (1=x*y) implx (0=1) implx (0=1) implx ((x=0) implx (0=1) implx (0=1)) implx (0=1)

toimplx(negx(y=1/x));
(%o52) (1=x*y) implx (0=1) implx (0=1) implx ((x=0) implx (0=1) implx (0=1)) implx (0=1)
 implx (0=1)

toimplx((0<=1/x)eqx(a<x));
(%o53) (0<x) implx (0=1) implx (0=1) implx ((0<=1) implx (0=1)) implx (0=1) implx (0=1) implx 
((x<0) implx (0=1) implx (0=1) implx ((1<=0) implx (0=1)) implx (0=1)) implx (0=1) implx (0=1)
 implx ((a<x) implx (0=1)) implx (0=1) implx (0=1) implx ((a<x) implx (0=1) implx (0=1) implx 
(0=1) implx ((0<x) implx (0=1) implx (0=1) implx ((0<=1) implx (0=1)) implx (0=1) implx (0=1)
 implx ((x<0) implx (0=1) implx (0=1) implx ((1<=0) implx (0=1)) implx (0=1)) implx (0=1)
 implx (0=1)) implx (0=1))

toimplx(((0<x) andx (0<y)) implx (x/y+y/x>=c));
(%o54) (0<x) implx (0=1) implx (0=1) implx ((0<y) implx (0=1)) implx (0=1) implx ((0<x*y)
 implx (0=1) implx (0=1) implx ((c*x*y<=y^2+x^2) implx (0=1)) implx (0=1) implx (0=1) implx 
((x*y<0) implx (0=1) implx (0=1) implx ((y^2+x^2<=c*x*y) implx (0=1)) implx (0=1)))