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

　量化記号all,exも使えるようにしました．すなわち，all(束縛変数,論理式)およびex(束縛変数,論理式)は論理式であり，all,exから始まる論理式はこの形に限ります．

　ただし，束縛変数は入力時に区別する必要があります（勝手にalpha-convしません．したがって，勝手に式をコピーするeqxとの併用や，他所で量化した式の利用は禁忌です）．出力はprenex normal formです．

map(infix,[implx,replx,orx,andx,eqx]);
matchdeclare([aa,bb,cc],true); 
aa replx bb:=(bb)implx(aa);
negx(aa):=(aa)implx(0=1);
aa orx bb:=(negx(aa))implx(bb);
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);
toimplx2(x):=toimplx1(toimplx1(x));

defrule(Fr1,(aa)implx(all(bb,cc)),all(bb,(aa)implx(cc)));
defrule(Fr2,(aa)implx(ex(bb,cc)),ex(bb,(aa)implx(cc)));
defrule(Fr3,(all(bb,aa))implx(cc),ex(bb,(aa)implx(cc)));
defrule(Fr4,(ex(bb,aa))implx(cc),all(bb,(aa)implx(cc)));
defrule(Fr5,(aa)implx(nf(bb,cc)),nf(bb,(aa)implx(cc)));
defrule(Fr6,(aa)implx(fn(bb,cc)),fn(bb,(aa)implx(cc)));
defrule(Fr7,(nf(bb,aa))implx(cc),fn(bb,(aa)implx(cc)));
defrule(Fr8,(fn(bb,aa))implx(cc),nf(bb,(aa)implx(cc)));

topnfx1(x):=applyb1(x,Fr1,Fr2,Fr3,Fr4,Fr5,Fr6,Fr7,Fr8);
topnfx(n,x):=if 1<n then topnfx1(topnfx(n-1,x)) else topnfx1(x);

toimplx(x):=topnfx(20,toimplx2(x));

入出力例

all(e,(0<e) implx ex(d,(0<d) andx all(x,((a-d<x) andx (x<a+d)) implx ((b-e<x^2) andx (x^2<b+e)))));
(%o30) all(e,(0<e) implx ex(d,(0<d) implx (0=1) implx (0=1) implx (all(x,(a-d<x) implx (0=1)
 implx (0=1) implx ((x<d+a) implx (0=1)) implx (0=1) implx 
((b-e<x^2) implx (0=1) implx (0=1) implx ((x^2<e+b) implx (0=1)) implx (0=1))) implx (0=1))
 implx (0=1)))

toimplx(%);
(%o31) all(e,ex(d,all(x,(0<e) implx ((0<d) implx ((a-d<x) implx ((x<d+a) implx (0=1)) implx 
(0=1) implx ((b-e<x^2) implx ((x^2<e+b) implx (0=1)) implx (0=1)) implx (0=1)) implx (0=1)))))