ATPとCASのこと

2015-08-04

nnscan

nns は最も外にある %and または %or に作用するのみなので

(%i1) nns(((x>=0)%and(x=0))%or((x>=1)%and(x=1)));
(%o1)         ((x = 0) %and (x >= 0)) %or ((x = 1) %and (x >= 1))
(%i2) nns((((x>=0)%and(x=0))%or((x>=1)%and(x=1)))%and((y>=0)%and(y=0)));
(%o2) (((x = 0) %and (x >= 0)) %or ((x = 1) %and (x >= 1))) %and (y = 0)

となってしまいます.

ということで,scanmap 版を作りました.

nns(f):=
block([cl,L,fk],cl(f,g):=length(f)<=length(g),
if atom(f) then return(f)
elseif op(f)="%and" then
 (L:sort(rest(full_listify(powerset(setify(args(f))))),cl), 
 for k:1 thru length(L) do
 (fk:substpart("%and",part(L,k),0),
 if qe([],(fk)%implies(f))=true then return(fk)))
elseif op(f)="%or" then
 (L:sort(rest(full_listify(powerset(setify(args(f))))),cl), 
 for k:1 thru length(L) do
 (fk:substpart("%or",part(L,k),0),
 if qe([],(f)%implies(fk))=true then return(fk)))
else f)$
nnscan(f):=scanmap(nns,f)$
(%i3) nnscan(%o1);
(%o3)                         (x = 0) %or (x = 1)
(%i4) nnscan(%o2);
(%o4)                 ((x = 0) %or (x = 1)) %and (y = 0)

scan ではなく,入力をまず連言or選言標準形に書き換えて nns するのが一般的でしょうが,果たして...

Connection: close