% ----------------------------------------------------------------------
% $Id: dcfsfkacem.red,v 1.4 2004/03/23 11:31:45 dolzmann Exp $
% ----------------------------------------------------------------------
% copyright (c) 2004 thomas sturm
% ----------------------------------------------------------------------
% $Log: dcfsfkacem.red,v $
% Revision 1.4 2004/03/23 11:31:45 dolzmann
% Corrected tags for cvs.
%
% revision 1.1 2004/03/22 12:31:49 sturm
% initial check-in.
% mostly copied from acfsf.
% includes diploma thesis by kacem plus wrapper for this.
%
% ----------------------------------------------------------------------
lisp <<
fluid '(dcfsfkacem_rcsid!* dcfsfkacem_copyright!*);
dcfsfkacem_rcsid!* := "$Id: dcfsfkacem.red,v 1.4 2004/03/23 11:31:45 dolzmann Exp $";
dcfsfkacem_copyright!* := "copyright (c) 2004 t. sturm"
>>;
module dcfsfkacem;
% diferentially closed field standard form.
% part 1
fluid '(dqe_counter!* !*dqeverbose !*dqegradord !*dqeoptqelim !*dqeoptsimp);
switch dqeverbose;
switch dqegradord;
switch dqeoptqelim;
switch dqeoptsimp;
on1 'dqeverbose;
on1 'dqegradord;
on1 'dqeoptqelim;
on1 'dqeoptsimp;
algebraic (for all x,n let df(x d n,x)=0);
% part 2
symbolic procedure dqe_isconstant(phi);
% is a constant. [phi] is differential polynomial. Returns nom-nil
% iff phi is a constant.
numberp phi or (pairp phi and car phi eq 'quotient and
numberp caddr phi and numberp reval cadr phi);
%%%%%%%%%%%%%% dqe_isatomarp %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% diese prozedur testet ob phi eine atomare formel ist. %
% (siehe kapitel 4 abschnitt 4.8) %
% %
% eingabe : beliebige formel phi . %
% %
% ausgabe : true falls phi atomar ist d.h. in sm. ist phi von %
% der form list(elem,f,g) wobei elem = equal %
% order neq und f,g differentiale polynome sind%
% false sonst . %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
procedure dqe_isatomarp(phi);
pairp phi and (car phi eq 'neq or car phi eq 'equal);
%%%%%%%%%%%%%% dqe_isquantfree %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% diese prozedur testet ob eine formel phi quantorenfrei ist. %
% (siehe kapitel 4 abschnitt 4.8) %
% %
% eingabe : beliebige formel phi . %
% %
% ausgabe : true falls phi quantorenfreie formel ist. %
% false sonst . %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_isquantfree(phi);
begin scalar erg;
if atom phi or (not phi) or dqe_isatomarp phi then
return T;
if car phi = 'nott then
return dqe_isquantfree cadr phi;
if car phi eq 'or or car phi eq 'and then <<
phi := cdr phi;
erg := T;
while erg and phi do <<
erg := dqe_isquantfree car phi;
phi := cdr phi
>>;
return erg;
>>;
return nil;
end;
%%%%%%%%%%%%%% dqe_isprenexp %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% diese prozedur testet ob eine formel phi in prenexform ist. %
% (siehe kapitel 4 abschnitt 4.8) %
% %
% eingabe : beliebige formel phi . %
% %
% ausgabe : true falls phi quantorenfrei ist oder phi von der %
% q_1 x_1...q_n x_n psi wobei q_i = ex oder all%
% und psi quantorenfrei ist. %
% false sonst . %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
procedure dqe_isprenexp(phi);
begin scalar erg;
if atom phi or (not phi) then
erg := t
else <<
while (car phi ='ex) or (car phi ='all) do
phi := caddr phi;
erg := dqe_isquantfree phi
>>;
return erg;
end;
%%%%%%%%%%%%%%%% dqe_modatomar %%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_modatomar ist eine sub-routine fuer dqe_helpelim. %
% (siehe kapitel 4 abschnitt 4.6) %
% %
% eingabe : atomare formel von der form "f = g" oder "not(f =g)"%
% %
% ausgabe : "f - g = 0" bzw "not(f - g = 0 )". %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
procedure dqe_modatomar(phi);
if caddr phi = 0 then
phi
else
{car phi,reval {'difference,cadr phi,caddr phi},0};
%%%%%%%%%%%%%%%% dqe_helpelim %%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_helpelim ist eine hilfsprozedur fuer dqe_elim. %
% (siehe kapitel 4 abschnitt 4.6) %
% %
% eingabe : eine teilformel phi. %
% %
% ausgabe : list(g) falls phi von der form not(g= 0) oder %
% g = g1*g2*..*gm und phi von der form %
% not(g1=0) and ...and not(gm=0) . %
% list(1,f) falls phi von der form f = 0 %
% list(1,f1,...,fn) falls phi von der form %
% f1 = 0 and ...and fn = 0 . %
% list(g,f1,...,fn) falls phi von der form %
% f1 = 0 and ...and fn = 0 and %
% not(g1=0) and ...and not(gm=0) %
% wobei g = g1*g2*..*gm . %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
procedure dqe_helpelim(phi);
begin scalar op;
if (phi eq t) or (not phi) then
return phi;
op := car phi;
if op eq 'neq then
return {reval cadr dqe_modatomar phi};
if op eq 'equal then
return {1,reval cadr dqe_modatomar phi};
if op eq 'and then
return dqe_helpelim!-and cdr phi;
rederr "dqe_helpelim: internal error";
end;
procedure dqe_helpelim!-and(phi);
begin scalar a,eqs,g;
g := 1;
while phi do <<
a := car phi;
if car a eq 'equal then
eqs := adjoin(reval cadr dqe_modatomar a,eqs)
else
g := reval {'times,g,reval cadr dqe_modatomar a};
phi := cdr phi
>>;
return g . reversip eqs
end;
%%%%%%%%%%%%%%%% dqe_andorvaleur %%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% and-or-valeur gibt bei einer disjunktion bzw. konjunktion %
% zweier formeln eine vereinfachte flache formel aus, die zur %
% disjunktion bzw. konjunktion aequivalent ist. %
% (siehe kapitel 4 abschnitt 4.9) %
% %
% eingabe : eine liste der form list(elem,phi,psi) %
% wobei elem = ' and oder elem = 'or. %
% %
% ausgabe : cons(elem,cons(phi,cdr psi) falls car psi = elem %
% und not(car phi = elem) . %
% %
% cons(elem,cons(psi,cdr phi) falls car phi = elem %
% und not(car psi = elem). %
% %
% appand(phi,cdr psi) falls car phi = car psi = elem. %
% %
% phi falls psi leer ist. %
% %
% psi falls phi leer ist. %
% %
% list(elem,phi,psi) sonst %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_andorvaleur(phi);
begin scalar erg,hilf,hilff,andor;
erg := nil;andor := car phi; hilf := cadr phi; hilff:= caddr phi;
if hilf
then
<<if hilff
then
<< if car hilf = andor
and car hilff = andor
then
<< hilf := reverse cdr hilf;
hilff := cdr hilff;
while hilf do
<< hilff := dqe_consm(car hilf,hilff);
hilf := cdr hilf >> ;
if not cdr hilff then erg := car hilff
else
erg := cons(andor,hilff) >>
else
if car hilf = andor
then erg := dqe_modcons(hilff,hilf)
else
if car hilff = andor
then erg := cons(andor,
dqe_consm(hilf,cdr hilff))
else erg := phi >>
else erg := hilf >>
else erg := hilff ;
return erg;
end;
%%%%%%%%%%%%%% dqe_consm %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% durch dieser prozedur wird jedes element nur einmal in der %
% liste eingetragen. %
% falls es schon in der liste enthalten ist, so bleibt die liste%
% unveraendert. (siehe kapitel 4 abschnitt 4.9) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_consm(elem,liste);
if elem member liste
then liste
else cons(elem,liste);
%%%%%%%%%%%%%% dqe_modcons %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% durch dieser prozedur wird jedes element nur einmel in der %
% liste eingetragen. %
% falls es schon in der liste enthalten ist, so bleibt die liste%
% unveraendert. sonst wird es an das ende der liste angehaengt. %
% (siehe kapitel 4 abschnitt 4.9) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_modcons(elem,liste);
if elem member liste
then liste
else reverse cons(elem,reverse liste);
% part 3
%%%%%%%%%%%%%%% dqe_makepositiveat %%%%%%%%%%%%%%%%%%%%%%%%%%%% %
% %
% diese prozedur wurde von k.d. burhenne uebernommen und ent- %
% sprechend geandert. (siehe kapitel 3 abschnitt 3.1) %
% dqe_makepositiveat berechnet bei eingabe einer negierten ato- % %
% maren formel die entsprechende aequivalente positive formel. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_makepositiveat (phi);
begin scalar psi;
psi := cadr phi;
return if car psi eq 'equal then
{'neq,cadr psi,caddr psi}
else
{'equal,cadr psi,caddr psi}
end;
%%%%%%%%%%%%%%% dqe_makepositive %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_makepositive berechnet zu einer gegebenen formel die ent- %
% sprechend aequivalente positive formel. %
% die rechenvorschrift fuer diese berechnung wurde von %
% k.d. burhenne uebernommen. anstelle der von burhenne verwen- %
% verwendeten stack-verwaltung bei der programmierung wurde %
% jedoch der rekursive programmierstil benutzt, d.h. die %
% positive formel wird durch rekursion ueber den aufbau von %
% formeln berechnet. (siehe kapitel 3 abschnitt 3.1) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_makepositive(formel);
begin scalar erg,hilfserg,hilf;
if (formel = t) or (not formel) then erg := formel
else
if car formel='nott
then
<< formel:=cadr formel;
if formel = t then erg := nil
else
if formel = nil then erg := t
else
if car formel='nott
then erg:=dqe_makepositive(cadr formel)
else
if car formel='ex
then <<erg:=dqe_makepositive(list('nott,caddr formel));
erg:=list('all,cadr formel,erg)>>
else
if car formel='all
then <<erg:=dqe_makepositive(list('nott,caddr formel));
erg:=list('ex,cadr formel,erg)>>
else
if car formel='and
then <<hilf:=cdr formel;hilfserg:=nil;
while hilf do
<<hilfserg:= dqe_makepositive(list('nott,car hilf));
erg := cons(hilfserg,erg);
hilf:=cdr hilf >>;
if cdr erg
then erg:=cons('or,reverse erg)>>
else
if car formel='or
then <<hilf:=cdr formel;hilfserg:=nil;
while hilf do
<<hilfserg:= dqe_makepositive(list('nott,car hilf));
erg := cons(hilfserg,erg);
hilf:=cdr hilf >>;
if cdr erg
then erg:=cons('and,reverse erg) >>
else
erg:=dqe_makepositiveat(list('nott,formel)) >>
else
<<
if car formel='ex
then <<erg:=dqe_makepositive(caddr formel);
erg:=list('ex,cadr formel,erg)>>
else
if car formel='all
then <<erg:=dqe_makepositive(caddr formel);
erg:=list('all,cadr formel,erg)>>
else
if car formel='and
then <<hilf:=cdr formel;hilfserg:=nil;
while hilf do
<<hilfserg:= dqe_makepositive(car hilf);
erg := cons(hilfserg,erg);
hilf:=cdr hilf >>;
if cdr erg
then erg:=cons('and,reverse erg)>>
else
if car formel='or
then <<hilf:=cdr formel;hilfserg:=nil;
while hilf do
<<hilfserg:= dqe_makepositive(car hilf);
erg := cons(hilfserg,erg);
hilf:=cdr hilf >>;
if cdr erg
then erg:=cons('or,reverse erg) >>
else erg:=formel >>;
return erg;
end;
%%%%%%%%%%%%%%% dqe_interchange7 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_interchange7 ist eine subroutine von dqe_makeprenex und wurde% %
% unveraendert von k.d. burhenne uebernommen. %
% sei l = (phi_1,...phi_n), wobei alle phi_j praenexe formeln %
% sind, %
% ls aus and,or , %
% a aus ex,all . %
% dann ist dqe_interchange7(l,ls,a) ein paar (phi,qb) mit folgenden %
% eigenschaften: %
% 1. phi ist wieder praenex und aequivalent zu %
% (phi_1 ls ... ls phi_n). %
% ferner ist fs(phi)=a, falls fs(phi_j)=a fuer ein j, d.h. %
% phi beginnt mit einem block von a-quantoren, falls moeglich. %
% 2. qb=qb(phi). %
% die prozedur dqe_interchange7 hat die eigenschaft, dass eine der %
% formeln dqe_interchange7(l,ls,ex), dqe_interchange7(l,ls,all) op- % %
% mal bzgl. der anzahl der quantorenbloecke ist, falls dies fuer %
% alle phi_j aus l schon der fall war. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_interchange7(l,ls,a);
begin scalar qlist,hilf,phi,qb,qb1,weiter;
qlist:=nil;weiter:=t;hilf:=nil; qb:=0;
while l do << hilf:=cons(caar l,hilf); l:=cdr l >>;
l:=hilf;
while weiter do
<< weiter:=nil;hilf:=nil;qb1:=0;
while l do
<< phi:=car l;l:=cdr l;
while car phi=a do
<< qlist:=cons(list(car phi,cadr phi),qlist);
phi:=caddr phi;qb1:=qb1+1 >>;
hilf:=cons(phi,hilf) >>;
l:=hilf;if qb1>0 then qb:=qb+1;
if a='ex then a:='all else a:='ex;
while hilf and not weiter do
<< if caar hilf='ex or caar hilf='all
then weiter:=t;
hilf:=cdr hilf >> >>;
phi:=cons(ls,l);
while qlist do << phi:=append(car qlist,list phi);
qlist:=cdr qlist >>;
return list(phi,qb)
end;
%%%%%%%%%%%%%%% dqe_pnfquantor %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% soubroutine von dqe_makeprenex, die unveraendert von %
% k.d. burhenne uebernommen wurde. %
% dqe_pnfquantor ist eine hilfsprozedur zur realisierung des %
% rekursionsschritts fuer dqe_pnf(siehe dort), %
% der erforderlich wird, wenn die eingabe phi mit %
% einem quantor beginnt, also etwa phi=ex(x,psi); %
% pnfquantor(phi) berechnet zunaechst die menge m=pnf(psi<n/x>),% ,%
% wobei n neuer identifikator ist, und berechnet daraus eine %
% optimale formel, die auch im hoeheren kontext optimal ist. %
% seiteneffekte:siehe unter dqe_pnf. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_pnfquantor(phi);
begin scalar erg,n,m,hilf,hilf1,z,dec;
dec:=car phi;
dqe_counter!*:=dqe_counter!*+1;z:=mkid('newid,dqe_counter!*);
erg:=dqe_pnf subst(z,cadr phi,caddr phi);
if cdr erg then
<<n:=cadr car erg;m:=cadr cadr erg;
if n<m then << hilf:=caar erg;hilf1:=list(dec,z,hilf);
if car hilf=dec then hilf1:=list(hilf1,n)
else hilf1:=list(hilf1,n+1);
erg:=list hilf1 >>
else
if n>m then << hilf:=caadr erg;hilf1:=list(dec,z,hilf);
if car hilf=dec then hilf1:=list(hilf,m)
else hilf1:=list(hilf,m+1);
erg:=list hilf1 >>
else << hilf:=erg;
while hilf and caaar hilf neq dec do
hilf:=cdr hilf;
if hilf
then << hilf:=list(list(dec,z,caar hilf),n);
erg:=list hilf >>
else << erg:=list(list(dec,z,caar erg),n+1);
erg:=list erg >> >> >>
else << if caaar erg neq dec then m:=cadar erg+1
else m:=cadar erg;
erg:=list list(list(dec,z,caar erg),m) >>;
return erg
end;
%%%%%%%%%% dqe_pnfjunktor %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% soubroutine von dqe_makeprenex, die unveraendert von %
% k.d. burhenne uebernommen wurde. %
% dqe_pnfjunktor ist eine hilfsprozedur zur realisierung des %
% rekursionsschritts fuer dqe_pnf (siehe dort), %
% der erforderlich wird, wenn fuer die eingabe phi gilt: %
% fs(phi) aus and,or, also etwa phi = phi_1 ls ... ls phi_n. %
% pnfjunktor(phi) berechnet zunaechst die mengen m_j=pnf(psi_j) % %
% und daraus das gewuenschte ergebnis. %
% seiteneffekte:siehe unter dqe_pnf. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_pnfjunktor(phi);
begin scalar erg,dec,hilf,hilf1,hilf2,psi,pair1,pair2,poss1,poss2,
l1,l2,m,m1;
dec:=car phi;m:=-1;poss1:=t;poss2:=t;hilf1:=nil;hilf2:=nil;
hilf:=cdr phi;l1:=nil;l2:=nil;
while hilf do << psi:=dqe_pnf car hilf;hilf:=cdr hilf;
hilf1:=cons(car psi,hilf1);
if cdr psi then hilf2:=cons(cadr psi,hilf2)
else hilf2:=cons(car psi,hilf2);
m1:=cadar psi;if m1>m then m:=m1 >>;
if m>0 then
<< while hilf1 do
<< pair1:=car hilf1;pair2:=car hilf2;
hilf1:=cdr hilf1;hilf2:=cdr hilf2;
l1:=cons(pair1,l1);l2:=cons(pair2,l2);
if cadr pair1=m and caar pair1 neq 'ex then poss1:=nil;
if cadr pair2=m and caar pair2 neq 'all then poss2:=nil >>;
if poss1 and not poss2
then erg:=list dqe_interchange7(l1,dec,'ex)
else if poss2 and not poss1
then erg:=list dqe_interchange7(l2,dec,'all)
else erg:=list(dqe_interchange7(l1,dec,'ex),
dqe_interchange7(l2,dec,'all)) >>
else erg:=list list(phi,0); return erg
end;
%%%%%%%%%%%%%%% dqe_pnf %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% soubroutine von dqe_makeprenex, die unveraendert von %
% k.d. burhenne uebernommen wurde. %
% pnf(phi) berechnet eine ein-oder zweielementige menge m von %
% praenexen formeln phi' derart,dass jede formel phi' in m aequi-%
% valent zu phi und optimal bzgl. der anzahl der quantorenbloecke%
% ist.in jedem fall ist eine der formeln aus m auch "im hoeheren %
% kontext" optimal. %
% falls #m=2, so beginnt eine formel mit einem existenzquantor %
% und eine mit einem allquantor. in der m darstellenden liste l %
% ist dann car l die formel, die mit einem existenzquantor %
% beginnt. die formeln werden so verwaltet, dass zusaetzlich die %
% anzahl der quantorenbloecke mitberechnet wird, d.h. %
% pnf(phi) ist entweder von der form %
% ( (phi_ex, qbex), (phi_all,qball)), %
% wobei phi_ex,phi_all die optimalen formeln sind, %
% qbex=qb(phi_ex) , qball=qb(phi_all), %
% oder von der form ((phi',qb)), wobei qb=qb(phi'). %
% verfahren : rekursion ueber den aufbau von phi. %
% falls phi atomar ist, wird ((phi,0)) ausgegeben. %
% ansonsten wird eine der prozeduren qnaquantor %
% oder qnajunktor aufgerufen, die die entsprechenden %
% rekursionsschritte(--> zunaechst rekursiver auf- %
% ruf von dqe_pnf) unter beibehaltung der %
% optimalitaet realisieren. %
% fuer die umbenennung von variablen greift dqe_pnf ueber qna- %
% quantor auf eine relativ globale variable counter zu. daraus %
% ergibt sich ein seiteneffekt an dieser variable. %
% dieser effekt ist jedoch unproblematisch, da pnf nur hilfs- %
% prozedur fuer die prozedur dqe_makeprenex ist, in der die %
% variable counter deklariert ist. letztere prozedur (nur diese %
% wird fuer weitere berechnungen verwendet) arbeitet ohne sei- %
% teneffekte. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_pnf(phi);
begin scalar dec,erg;
dec:=car phi;
if dec='ex or dec='all then erg:=dqe_pnfquantor phi
else
if dec='or or dec='and then erg:=dqe_pnfjunktor phi
else erg:=list list(phi,0);
return erg;
end;
%%%%%%%%%%%%%% dqe_makeprenex %%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_makeprenex berechnet zu einer gegebenen positiven formel %
% eine aequivalente praenexe formel, die optimal ist bzgl. der %
% anzahl der quantorenbloecke. %
% diese prozedur wurde unveraendert von k.d. burhenne ueber- %
% nommen. (siehe auch kapitel 3) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_makeprenex(phi);
begin scalar erg;
dqe_counter!*:=0;erg:=dqe_pnf phi;
if cdr erg then << if cadr car erg<= cadr cadr erg
then erg:=caar erg
else erg:=caadr erg >>
else erg:=caar erg;
return erg
end;
%%%%%%%%%%%%%%% dqe_pnfquantormod %%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% pnfquantormod ist eine subroutine fuer pnfmod. sie arbeitet % %
% wie dqe_pnfquantor (siehe kapitel 3 abschnitt 3.2). %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_pnfquantormod(phi,liste);
begin scalar erg,n,m,hilf,hilf1,z,dec;
dec:=car phi;
dqe_counter!*:=dqe_counter!*+1;z:=mkid('newid,dqe_counter!*);
liste := cons(cadr phi,cons(z,liste));
erg:= dqe_pnfmod(subst(z,cadr phi,caddr phi),liste);
liste := cadr erg;
erg := car erg;
if cdr erg then
<<n:=cadr car erg;m:=cadr cadr erg;
if n<m then << hilf:=caar erg;hilf1:=list(dec,z,hilf);
if car hilf=dec then hilf1:=list(hilf1,n)
else hilf1:=list(hilf1,n+1);
erg:=list hilf1 >>
else
if n>m then << hilf:=caadr erg;hilf1:=list(dec,z,hilf);
if car hilf=dec then hilf1:=list(hilf,m)
else hilf1:=list(hilf,m+1);
erg:=list hilf1 >>
else << hilf:=erg;
while hilf and caaar hilf neq dec do
hilf:=cdr hilf;
if hilf
then << hilf:=list(list(dec,z,caar hilf),n);
erg:=list hilf >>
else << erg:=list(list(dec,z,caar erg),n+1);
erg:=list erg >> >> >>
else << if caaar erg neq dec then m:=cadar erg+1
else m:=cadar erg;
erg:=list list(list(dec,z,caar erg),m) >>;
return list(erg,liste);
end;
%%%%%%%%%% dqe_pnfjunktormod %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%pnfjunktormod ist eine subroutine fuer dqe_pnfmod. sie arbeitet% %
% wie dqe_pnfjunktor (siehe kapitel 3 abschnitt 3.2). %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_pnfjunktormod(phi,liste);
begin scalar erg,dec,hilf,hilf1,hilf2,psi,pair1,pair2,poss1,poss2,
l1,l2,m,m1;
dec:=car phi;m:=-1;poss1:=t;poss2:=t;hilf1:=nil;hilf2:=nil;
hilf:=cdr phi;l1:=nil;l2:=nil;
while hilf do << psi:=dqe_pnfmod(car hilf,liste);
liste := cadr psi;
psi := car psi;
hilf:=cdr hilf;
hilf1:=cons(car psi,hilf1);
if cdr psi then hilf2:=cons(cadr psi,hilf2)
else hilf2:=cons(car psi,hilf2);
m1:=cadar psi;if m1>m then m:=m1 >>;
if m>0 then
<< while hilf1 do
<< pair1:=car hilf1;pair2:=car hilf2;
hilf1:=cdr hilf1;hilf2:=cdr hilf2;
l1:=cons(pair1,l1);l2:=cons(pair2,l2);
if cadr pair1=m and caar pair1 neq 'ex then poss1:=nil;
if cadr pair2=m and caar pair2 neq 'all then poss2:=nil >>;
if poss1 and not poss2
then erg:=list(list dqe_interchange7(l1,dec,'ex),liste)
else if poss2 and not poss1
then erg:=list(list(dqe_interchange7(l2,dec,'all)),liste)
else erg:=list(list(dqe_interchange7(l1,dec,'ex),
dqe_interchange7(l2,dec,'all)),liste) >>
else erg:=list(list(list(phi,0)),liste); return erg
end;
%%%%%%%%%%%%%%% dqe_pnfmod %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%pnfmod ist eine subroutine fuer makeprenexmod. sie arbeitet % %
% wie dqe_pnf (siehe kapitel 3 abschnitt 3.2). %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_pnfmod(phi,liste);
begin scalar dec,erg;
dec:=car phi;
if dec='ex or dec='all then erg:=dqe_pnfquantormod(phi,liste)
else
if dec='or or dec='and then erg:=dqe_pnfjunktormod(phi,liste)
else erg:=list(list(list(phi,0)),liste);
return erg;
end;
%%%%%%%%%% dqe_makeprenexmod %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% makeprenexopt arbeitet genau wie makeprenex. sie berechnet zu % u %
% einer gegebnen positeven formel die selbe aequivalente prae- %
% nexe formel wie bei dqe_makeprenex. %
% sie berechnetet noch dazu die up-dating der liste diffequa- %
% liste (siehe auch kapitel 3 abschnitt 3.2). %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_makeprenexmod(phi,diffequaliste);
begin scalar erg,hilfliste,liste,ausg;
scalar var,newvar,hilf;
ausg := nil;
dqe_counter!*:=0;
liste := nil;
hilfliste := diffequaliste;
erg:=dqe_pnfmod(phi,liste);
liste := cadr erg;
erg := car erg;
if cdr erg then << if cadr car erg<= cadr cadr erg
then erg:=caar erg
else erg:=caadr erg >>
else erg:=caar erg;
while liste do
<< var := car liste;
newvar := cadr liste;
liste := cddr liste;
hilfliste := subst(newvar,var,hilfliste) >>;
while hilfliste do
<< var := car hilfliste;
hilf := cadr hilfliste;
hilfliste := cddr hilfliste;
if not(var member diffequaliste)
then diffequaliste := cons(var,
cons(hilf,diffequaliste)) >>;
ausg := list(erg,diffequaliste);
return ausg;
end;
%%%%%%%%%%%%%%% dqe_disjnf %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_dnfjnf berechnet eine disjunktive normalform einer positi-%
% ven quantorenfreien formel. %
% (siehe kapitel 3 abschnitt 3.3) %
% vorgehen: %
% 1.: formel = t oder nil --> stop %
% 2.: formel = (and ...) --> aufruf dqe_distributiv formel %
% 3.: formel = (or ...) --> fuer alle teilformeln %
% aufruf dqe_disjnf %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_disjnf(formel);
begin scalar erg,hilf;
erg := nil;
if (formel = t) or (not formel)
or dqe_isatomarp(formel)
then erg := formel
else
if car formel ='and
then erg := dqe_distributiv(formel)
else
if car formel ='or
then
<< formel := cdr formel;
while formel do
<< hilf := car formel; formel := cdr formel;
hilf := dqe_disjnf(hilf);
if (hilf = t) or (not hilf)
or
dqe_isatomarp(hilf) or (car hilf = 'and)
then
<< if not erg then erg := list(hilf)
else
if not cdr(erg)
then
<< if not(hilf = car erg)
then erg := list('or,
car erg,hilf) >>
else erg := dqe_modcons(hilf,erg) >>
else
<< if length erg = 1
then erg := car erg;
erg := dqe_andorvaleur
list('or,erg,hilf) >> >>;
if length erg = 1 then erg := car erg>>
else erg := formel;
if !*dqeoptsimp then erg := dqe_dknfsimplify(erg);
return erg;
end;
%%%%%%%%%%%%%%% dqe_konjnf %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_konjnf berechnet eine konjunktive normalform einer positi-%
% ven quantorenfreien formel. %
% (siehe auch kapitel 3 abschnitt 3.3) %
% vorgehen: %
% 1.: formel = t oder nil --> stop %
% 2.: formel = (or ...) --> aufruf dqe_distributiv formel %
% 3.: formel = (and ...) --> fuer alle teilformeln %
% aufruf dqe_konjnf %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_konjnf(formel);
begin scalar erg,hilf;
erg := nil;
if (formel = t) or (not formel)
or dqe_isatomarp(formel)
then erg := formel
else
if car formel ='or
then erg := dqe_distributiv(formel)
else
if car formel ='and
then
<< formel := cdr formel;
while formel do
<< hilf := car formel; formel := cdr formel;
hilf := dqe_konjnf(hilf);
if (hilf = t) or (not hilf)
or
dqe_isatomarp(hilf) or (car hilf = 'or)
then
<< if not erg then erg := list(hilf)
else
if not cdr(erg)
then
<< if not(hilf = car erg)
then erg := list('and,
car erg,hilf) >>
else erg := dqe_modcons(hilf,erg) >>
else
<< if length erg = 1
then erg := car erg;
erg := dqe_andorvaleur
list('and,erg,hilf) >> >>;
if length erg = 1 then erg := car erg>>
else erg := formel;
if !*dqeoptsimp
then erg := dqe_dknfsimplify(erg);
return erg;
end;
%%%%%%%%%%%%%%% dqe_distributiv %%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% sub-routine von dqe_disjnf und dqe_konjnf zur anwendung der % %
% distributivgesetze. %
% (siehe auch kapitel 3 abschnitt 3.3) %
% vorgehen: %
% 1.fall: eingabe: (or ...) %
% ausgabe: (and phi_1 phi_2 ...) , %
% wobei phi_1, phi_2, ... keine and's enthalten.%
% 2.fall: eingabe: (and ...) %
% ausgabe: (or phi_1 phi_2 ...) , %
% wobei phi_1, phi_2, ... keine or's enthalten.%
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_distributiv(formel);
begin scalar symb1,symb2,ausg,hilf1,hilf2,hilf,hilf3,hilff;
symb1 := car formel; ausg := nil;
if symb1='or
then symb2 := 'and
else symb2 := 'or;
formel := cdr formel;
while formel do
<< hilf := car formel; formel := cdr formel;
if (hilf = t) or not(hilf)
or dqe_isatomarp(hilf)
then
<< if not ausg
then ausg := cons(hilf,ausg)
else
if not cdr ausg
then
<< hilf1 := car ausg;
if not( hilf = hilf1)
then ausg := list(symb1,hilf1,hilf) >>
else
if car ausg = symb1
then ausg := dqe_modcons(hilf,ausg)
else
<< hilf1 := cdr ausg; ausg := nil;
while hilf1 do
<< hilf2 := car hilf1;
hilf1 := cdr hilf1;
if (hilf2 = t) or not hilf2
or dqe_isatomarp(hilf2)
then
<<if not( hilf2 = hilf1)
then hilf2 := list(symb1,hilf2,hilf) >>
else hilf2 := dqe_modcons(hilf,hilf2);
ausg := dqe_modcons(hilf2,ausg) >>;
if cdr ausg
then ausg := cons(symb2,ausg) >> >>
else
if car hilf = symb1
then
<< hilf := dqe_distributiv(hilf);
if (hilf = t) or not(hilf)
or dqe_isatomarp(hilf)
then
<<if not ausg
then ausg := cons(hilf,ausg)
else
if not cdr ausg
then
<<hilf1 := car ausg;
if not( hilf = hilf1)
then ausg := list(symb1,hilf1,hilf) >>
else
if car ausg = symb1
then ausg := dqe_modcons(hilf,ausg)
else
<<hilf1 := cdr ausg; ausg := nil;
while hilf1 do
<<hilf2 := car hilf1;
hilf1 := cdr hilf1;
if (hilf2 = t) or not hilf2
or dqe_isatomarp(hilf2)
then
<<if not( hilf2 = hilf1)
then hilf2 :=
list(symb1,hilf2,hilf) >>
else hilf2 :=
dqe_modcons(hilf,hilf2);
ausg := dqe_modcons(hilf2,ausg) >>;
if cdr ausg
then ausg := cons(symb2,ausg)>> >>
else
if car hilf = symb1
then
<< if not ausg
then ausg := hilf
else
if not cdr ausg
then ausg := cons(symb1,dqe_consm(car ausg,cdr hilf))
else
if car ausg = symb1
then ausg := dqe_andorvaleur
list(symb1,ausg,hilf)
else
<< hilf1 := cdr ausg; ausg := nil;
while hilf1 do
<< hilf2 := car hilf1; hilf1 := cdr hilf1;
if (hilf2 = t) or (not hilf2)
or dqe_isatomarp(hilf2)
then hilf2 := list(symb1,
dqe_consm(hilf2,cdr hilf))
else hilf2 := dqe_andorvaleur
list(symb1,hilf2,hilf);
ausg := dqe_modcons(hilf2,ausg) >>;
if cdr ausg
then ausg := cons(symb2,ausg) >> >>
else
<< if not ausg
then ausg := hilf
else
if not cdr ausg
then
<< hilf1 := car ausg; ausg := nil;
hilf := cdr hilf;
while hilf do
<< hilf2 := car hilf; hilf := cdr hilf;
if (hilf2 = t) or (not hilf2)
or dqe_isatomarp hilf2
then
<<if not(hilf1 = hilf2)
then hilf2 := list(symb1,hilf1,hilf2)>>
else
hilf2 := cons(symb1,dqe_consm(hilf1,cdr hilf2));
ausg := dqe_modcons(hilf2,ausg) >>;
if cdr ausg
then ausg := cons(symb2,ausg)>>
else
if car ausg = symb2
then
<< hilf1 := cdr ausg; ausg := nil;
while hilf1 do
<< hilf2 := car hilf1; hilf1 := cdr hilf1;
hilff := cdr hilf;
while hilff do
<< hilf3 := car hilff; hilff := cdr hilff;
if (hilf2 = t) or (not hilf2)
or dqe_isatomarp hilf2
then
<<if (hilf3 = t) or (not hilf3)
or dqe_isatomarp hilf3
then
<< if not(hilf3 = hilf2)
then hilf3 := list(symb1,
hilf2,hilf3) >>
else
<< hilf3 := dqe_consm(hilf2,cdr hilf3);
hilf3 := cons(symb1,hilf3) >> >>
else
<<if (hilf3 = t) or (not hilf3)
or dqe_isatomarp hilf3
then
hilf3 := dqe_modcons(hilf3,hilf2)
else hilf3 := dqe_andorvaleur
list(symb1,hilf2,hilf3) >>;
ausg := dqe_modcons(hilf3,ausg) >> >>;
if cdr ausg
then ausg := cons(symb2,ausg) >>
else
<< hilf := cdr hilf;
hilf1 := ausg; ausg := nil;
while hilf do
<< hilf2 := car hilf; hilf := cdr hilf;
if (hilf2 = t) or (not hilf2)
or dqe_isatomarp hilf2
then
hilf2 := dqe_modcons(hilf2,hilf1)
else hilf2 := dqe_andorvaleur
list(symb1,hilf1,hilf2);
ausg := dqe_modcons(hilf2,ausg) >>;
if cdr ausg
then ausg := cons(symb2,ausg) >> >> >>
else
<< if symb2 = 'or
then hilf := dqe_disjnf(hilf)
else hilf := dqe_konjnf(hilf);
if (hilf = t) or not(hilf)
or dqe_isatomarp(hilf)
then
<<if not ausg
then ausg := cons(hilf,ausg)
else
if not cdr ausg
then
<<hilf1 := car ausg;
if not( hilf = hilf1)
then ausg := list(symb1,hilf1,hilf) >>
else
if car ausg = symb1
then ausg := dqe_modcons(hilf,ausg)
else
<<hilf1 := cdr ausg; ausg := nil;
while hilf1 do
<<hilf2 := car hilf1;
hilf1 := cdr hilf1;
if (hilf2 = t) or not hilf2
or dqe_isatomarp(hilf2)
then
<<if not( hilf2 = hilf1)
then hilf2 :=
list(symb1,hilf2,hilf) >>
else hilf2 :=
dqe_modcons(hilf,hilf2);
ausg := dqe_modcons(hilf2,ausg) >>;
if cdr ausg
then ausg := cons(symb2,ausg)>> >>
else
if car hilf = symb2
then
<< if not ausg
then ausg := hilf
else
if not cdr ausg
then
<< hilf1 := car ausg; ausg := nil;
hilf := cdr hilf;
while hilf do
<< hilf2 := car hilf; hilf := cdr hilf;
if (hilf2 = t) or (not hilf2)
or dqe_isatomarp(hilf2)
then
<< if not(hilf2 = hilf1)
then hilf2 := list(symb1,
hilf1,hilf2)>>
else hilf2 := cons(symb1,
dqe_consm(hilf1,cdr hilf2));
ausg := dqe_modcons(hilf2,ausg) >>;
if cdr ausg
then ausg := cons(symb2,ausg) >>
else
if car ausg = symb2
then
<< hilf1 := cdr ausg; ausg := nil;
while hilf1 do
<< hilf2 := car hilf1; hilf1 := cdr hilf1;
hilff := cdr hilf;
while hilff do
<< hilf3 := car hilff; hilff := cdr hilff;
if (hilf2 = t) or (not hilf2)
or dqe_isatomarp hilf2
then
<<if (hilf3 = t) or (not hilf3)
or dqe_isatomarp hilf3
then
<< if not(hilf2 = hilf3)
then hilf3 := list(symb1,
hilf2,hilf3) >>
else
<< hilf3 :=dqe_consm(hilf2,cdr hilf3);
hilf3 := cons(symb1,hilf3) >> >>
else
<<if (hilf3 = t) or (not hilf3)
or dqe_isatomarp hilf3
then
hilf3 := dqe_modcons(hilf3,hilf2)
else hilf3 := dqe_andorvaleur
list(symb1,hilf2,hilf3) >>;
ausg := dqe_modcons(hilf3,ausg) >> >>;
if cdr ausg
then ausg := cons(symb2, ausg) >>
else
<< hilf1 := ausg; ausg := nil;
hilf := cdr hilf;
while hilf do
<< hilf2 := car hilf; hilf := cdr hilf;
if (hilf2 = t) or (not hilf2)
or dqe_isatomarp(hilf2)
then hilf2 := dqe_modcons(hilf2,hilf1)
else hilf2 := dqe_andorvaleur
list(symb1,hilf1,hilf2);
ausg := dqe_modcons(hilf2,ausg) >>;
if cdr ausg
then ausg := cons(symb2,ausg) >> >>
else %car hilf = symb1%
<<if not ausg
then ausg := hilf
else
if not cdr ausg
then ausg := cons(symb1,dqe_consm(car ausg,cdr hilf))
else
if car ausg = symb1
then ausg := dqe_andorvaleur
list(symb1,ausg,hilf)
else
<< hilf1 := cdr ausg; ausg := nil;
while hilf1 do
<< hilf2 := car hilf1; hilf1 := cdr hilf1;
if (hilf2 = t) or (not hilf2)
or dqe_isatomarp(hilf2)
then hilf2 := cons(symb1,
dqe_consm(hilf2,cdr hilf))
else hilf2 :=
dqe_andorvaleur list(symb1,hilf2,hilf);
ausg := dqe_modcons(hilf2,ausg) >>;
if cdr ausg
then ausg := cons(symb2,ausg) >> >>
>> >>;
if length ausg = 1
then ausg := car ausg;
return ausg;
end;
%%%%%%%%%%%%%%% dqe_simplifyat %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% diese prozedur wurde von k.d. burhenne uebernommen und ent- %
% sprechend den hier auftretenden atomaren formeln angepasst. %
% dqe_simplifyat versucht eine atomare formel aussagenlogisch zu%
% vereinfachen, d.h. es wird versucht die atomare formel, falls %
% moeglich zu true oder false auszuwerten. (siehe abschnitt 3.4)%
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_simplifyat(phi);
begin scalar diff,erg,hilf,liste;
if (atom phi) or (not phi)
then erg:=phi
else
<< diff:= cadr phi;
if dqe_isconstant diff
then erg:= eval list(car phi,diff,0)
else
if listp diff
then
<< if car diff ='minus or car diff = 'expt
then
<< diff := cadr diff;
erg := dqe_simplifyat(list(car phi,diff,0))>>
else
if car diff ='times
then
<< diff := cdr diff;
while diff do
<< hilf := car diff;
if not(dqe_isconstant hilf)
then liste := dqe_consm(hilf,liste);
diff := cdr diff >>;
if not liste
then erg := eval list(car phi,1,0)
else
if not cdr liste
then erg := list(car phi,car liste,0)
else
<< while liste do
<< hilf := car liste; liste := cdr liste;
hilf :=dqe_simplifyat(list(car phi,hilf,0));;
erg := dqe_modcons(hilf,erg) >>;
if not cdr erg then erg := car erg
else
if car phi = 'neq
then erg := cons('and,erg)
else erg := cons('or,erg) >> >>
else
if car diff = 'plus
then
<< hilf := qe92_lin_normcontent diff;
if not( hilf = 1)
then diff := reval list('quotient,diff, hilf);
if minusf numr simp diff
then diff := reval list('minus,diff);
erg := list(car phi,diff,0) >>
else erg := list(car phi,diff,0) >>
else erg := phi>>;
return erg;
end;
%%%%%%%%%%%%%%% dqe_simplify %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_simplify vereinfacht eine positive quantorenfreie formel %
% mit abstuetzung auf dqe_simplifyat durch rekursion ueber den %
% aufbau der formel. %
% diese prozedur wurde von k.d. burhenne uebernommen und %
% entsprechend geaendert. (siehe kapitel 3 abschnitt 3.4) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_simplify(phi);
begin scalar erg,hilf,erghilf,weiter;
if (phi = t) or (not phi)
then erg := phi
else
if car phi ='and
then
<< weiter:=t;hilf:=cdr phi;erg:=nil;
while weiter and hilf do
<< erghilf:=dqe_simplify car hilf;hilf:=cdr hilf;
if erghilf=nil
then weiter:=nil
else
if erghilf neq t
then erg:= dqe_modcons(erghilf,erg) >>;
if weiter=nil then erg:= nil
else
if not erg then erg:= t
else
if cdr erg
then erg:=cons('and, erg)
else erg:=car erg >>
else
if car phi ='or
then
<< weiter:=t;hilf:=cdr phi;erg:=nil;
while weiter and hilf do
<< erghilf:=dqe_simplify car hilf;hilf:=cdr hilf;
if erghilf=t
then weiter:=nil
else
if erghilf neq nil
then erg:=dqe_modcons(erghilf,erg) >>;
if weiter=nil then erg:= t
else
if not erg then erg:= nil
else
if cdr erg then erg:=cons('or, erg)
else erg:=car erg >>
else erg:=dqe_simplifyat phi ;
if !*dqeoptsimp
then erg := dqe_helpsimplify(erg);
return erg ;
end;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% die folgenden prozeduren wurden unveraendert aus der arbeit %
% qe92 von t. sturm uebernommen. %
% die procedur qe92_lin_normconten berechnet den zahligen ggt.%
% aller monomen eines gegebenen polynomes. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure qe92_lin_normcontent u;
prepf qe92_lin_normcontent1(numr simp u,nil);
symbolic procedure qe92_lin_normcontent1(u,g);
% g is the gcd collected so far.
if g = 1 then g
else if domainp u then gcdf(absf u,g)
else qe92_lin_normcontent1(red u,qe92_lin_normcontent1(lc u,g));
% part 4
%%%%%%%%%%%%%%%% dqe_helpremainder %%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_helpremainder ist eine hilfsprozedur fuer dqe_restfkt.sie%
% ist eine umbennenung fuer die reduce-funktion remainder, die %
% nur im algebraischen modus verwendet werden kann. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
algebraic procedure dqe_helpremainder(phi,psi,var);
begin scalar erg;
korder var;
erg := remainder(phi,psi);
return erg;
end;
%%%%%%%%%%%%%%%%% dqe_ helpcoeff %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_helpcoeff ist eine hilfsprozedur fuer dqe_koeff. sie ist %
% eine umbennenung der reduce-funktion coeff, die nur im alge- %
% braischen modus verwendet werden kann. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
algebraic procedure dqe_helpcoeff(phi,var);
begin scalar erg;
erg := coeff(phi,var);
return erg;
end;
%%%%%%%%%%%%%%%%%%%% dqe_koeff %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%dqe_koeff ist eine hilfsprozedur fuer dqe_termcoefkt.sie bestimmt%
% die liste der koeffizienten eines differentialpolynoms phi %
% bzgl. der variable var.sie verwendet die hilfsprozedur dqe_help-%
% coeff. (siehe kapitel 4 abschnitt 4.5) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_koeff(phi,var);
begin scalar erg;
erg := cdr reval dqe_helpcoeff(phi,var);
return erg;
end;
%%%%%%%%%%%%%%%%%%%% dqe_restfkt %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%dqe_restfkt ist eine hilfsprozedur fuer dqe_termcoefkt.sie bestimmt%
% den rest der divition eines differentialpolynoms phi durch %
% ein differentialpolynom psi bzgl. der variable var. sie verwendet %
% die hilfsprozedur dqe_helpremainder. %
% (siehe kapitel 4 abschnitt 4.5) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_restfkt(phi,psi,var);
begin scalar erg;
erg := dqe_pform dqe_helpremainder(phi,psi,var);
if not erg then erg := 0;
return erg;
end;
%%%%%%%%%%%%%%%%% dqe_pseudf %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%dqe_pseudf ist eine hilfsprozedur fuer dqe_partialdf.sie bestimmt%
% die normale partialableitung eines differentialpolynoms phi %
% bzgl. der variable var.sie verwendet die hilfsprozedur dqe_help-%
% df. (siehe kapitel 4 abschnitt 4.2) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_pseudf(phi,var);
reval {'df,phi,var};
%%%%%%%%%%%%%%%%%% dqe_varmengefkt %%%%%%%%%%%%%%%%%%%%%%%%
% %
% varmengefkt berechnet die menge aller im differentialpolynom %
% vorkommenden variablen. (siehe kapitel 4 abschnitt 4.2) %
% %
% eingabe : ein differentialpolynom phi. %
% %
% ausgabe : eine liste der allen variablen, die in phi %
% vorkommen . %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_varmengefkt(phi);
begin scalar varmenge,hilf,elem,hilfmenge;
hilf := phi;
varmenge := nil;
if atom hilf
then << if not dqe_isconstant hilf
then varmenge := list(hilf)>>
else
if car hilf = 'd
then varmenge := list(hilf)
else
<<while hilf do
<< elem := car hilf;
hilf := cdr hilf;
if atom elem
then
<< if not(elem ='plus or elem ='times or elem ='expt
or elem ='minus or dqe_isconstant elem )
then varmenge := dqe_modcons(elem,varmenge)>>
else
<< hilfmenge := dqe_varmengefkt(elem);
while hilfmenge do
<< varmenge := dqe_modcons(car hilfmenge,varmenge);
hilfmenge := cdr hilfmenge >> >> >> >>;
return varmenge;
end;
%%%%%%%%%%%%%%%%%%%% dqe_partieldf %%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% die prozedur dqe_partieldf berechnet die partielle ableitung %
% von phi bezueglich der variable var . %
% die liste diffequaliste ist leer oder sie besteht aus einer %
% liste von der form list(var_1,var_1',var_2,var_2',...) wobei %
% die ableitung von var_k gleich var_k' ist. %
% (siehe kapitel 4 abschnitt 4.2) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_partieldf(phi,var,diffequaliste);
begin scalar hilf,liste,ausg;
ausg := 0;
hilf := dqe_pseudf(phi,var);
if not(var member diffequaliste)
then
<< if atom var
then ausg := reval list('times,hilf,list('d,var,1))
else ausg := reval list('times,hilf,list('d,cadr var,
eval list('plus,caddr var,1))) >>
else
<< liste := diffequaliste;
while not(var = car liste) do << liste := cddr liste >>;
if cadr liste = 0
then ausg := 0
else ausg := reval list('times,hilf,cadr liste) >>;
return ausg;
end;
%%%%%%%%%%%%%%%% dqe_diffkt %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%dqe_diffkt berechnet die erste ableitung des differentialpoly-%
% nomes phi. sie ist eine sub-routine von dqe_diff. %
% (siehe kapitel 4 abschnitt 4.2) %
% %
% eingabe : phi und diffequaliste. %
% ausgabe : die ableitung von phi . %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_diffkt(phi,diffequaliste);
begin scalar var,varmenge,hilf,erg;
erg := nil;
varmenge := dqe_varmengefkt(phi);
while varmenge do
<< var := car varmenge;
varmenge := cdr varmenge;
hilf := dqe_partieldf(phi,var,diffequaliste);
if not(hilf = 0)
then erg := cons(hilf,erg) >>;
if not erg
then erg := 0
else
if not cdr erg
then erg := car erg
else erg := reval cons('plus,erg);
return erg ;
end;
%%%%%%%%%%%%%%%%%% dqe_diff %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% die prozedur dqe_diff berechnet die n_te ableitung des diffe-%
% rentialpolynoms phi. (siehe kapitel 4 abschnitt 4.2) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_diff(phi,const,diffequaliste);
begin scalar hilf, erg;
erg := phi;
hilf := 1;
while const >= hilf do
<< erg := dqe_diffkt(erg,diffequaliste);
hilf := hilf +1 >>;
return erg;
end;
%%%%%%%%%%%%%%%% dqe_termcoefkt %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_termcoefkt bestimmt die liste von koeffizienten der terme %
% eines differentialpolynoms bzgl. der variable var. %
% (siehe kapitel 4 abschnitt 4.5) %
% %
% eingabe : ein differentialpolynom phi und eine variable var . %
% %
% ausgabe : list(c1,c2,...,cn) wobei phi =c1*t1+c2*t2+...+cn*tn %
% und die ti's die terme von phi sind. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_termcoefkt(phi,var);
begin scalar hilf,ordc,rest,const,erg,ausg;
ausg := nil;
ordc := dqe_ord(phi,var);
rest := dqe_restfkt(phi,var,var);
const := 1;
if not(ordc = 0) and not(rest = 0)
then
while const <= ordc do
<< rest :=dqe_restfkt(rest,list('d,var,const),list('d,var,const));
if rest = 0
then const := ordc + 1
else const := const + 1 >> ;
hilf := reval list('difference,phi,rest);
hilf := dqe_koeff(hilf,var);
const := 1;
while const <= ordc do
<< while hilf do
<< if not(car hilf = 0)
then << erg := dqe_koeff(car hilf,list('d,var,const));
ausg := append(ausg,erg) >>;
hilf := cdr hilf >>;
hilf := ausg;
ausg := nil;
const := const + 1>>;
while hilf do
<< if not(car hilf = 0)
then ausg := dqe_modcons(car hilf,ausg);
hilf := cdr hilf >>;
ausg := cons(rest,ausg);
return ausg;
end;
%%%%%%%%%%%%%%%%% dqe_helpord %%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_helpord ist eine hilfsprozedur fuer dqe_ord.sie berechnet%
% die ordnung eines monomes phi bzgl. der variable var. %
% (siehe kapitel 4 abschnitt 4.3) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_helpord(phi,var);
begin scalar erg, hilf;
erg := 0;
if atom phi
then erg := 0
else
if car phi = 'd
then
<< if cadr phi = var
then erg := caddr phi
else erg := 0 >>
else
if car phi = 'expt
then erg := dqe_helpord(cadr phi,var)
else
if car phi ='minus
then erg := dqe_helpord(cadr phi,var)
else
if car phi = 'times
then
<< phi := cdr phi; erg := 0;
while phi do
<< hilf := car phi;
phi := cdr phi;
hilf := dqe_helpord(hilf,var);
erg := erg + hilf>> >>
else erg := 0;
return erg;
end;
%%%%%%%%%%%%%%%%%%%% dqe_ord %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%dqe_ord bestimmt die ordnung eines diffedifferentialpolynoms%
% phi bezueglich der variable var. %
% (siehe kapitel 4 abschnitt 4.3) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_ord(phi,var);
begin scalar ausg,hilf;
ausg := 0;
if atom phi
then ausg := 0
else
if not(car phi = 'plus )
then ausg := dqe_helpord(phi,var)
else
<< phi := cdr phi;
while phi do
<< hilf := car phi;
phi := cdr phi;
hilf := dqe_helpord(hilf,var);
if ausg < hilf
then ausg := hilf >> >>;
return ausg;
end;
%%%%%%%%%%%%%%%%%%% dqe_grad %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% die prozedur dqe_grad berechnet den grad des differential-%
% polynoms phi bezueglich der variable var . %
% (siehe kapitel 4 abschnitt 4.3) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_grad(phi,var);
begin scalar erg,hilf,ordc;
ordc := dqe_ord(phi,var);
if ordc = 0 then hilf := var
else hilf := list('d,var,ordc);
erg := deg(phi,hilf);
if null erg then erg := 0;
return erg;
end;
%%%%%%%%%%%%%%%%% dqe_initial %%%%%%%%%%%%%%%%%%%%%%%%%
% %
% die prozedur dqe_initial berechnet die initiale des diffe-%
% rentialpolynomes bezueglich der variable var . %
% (siehe kapitel 4 abschnitt 4.4) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_initial(phi,var);
begin scalar ordc,hilfvar,ausg;
ordc := dqe_ord(phi,var);
if ordc = 0 then hilfvar := var
else hilfvar := list('d,var,ordc);
ausg := reval lcof(phi,hilfvar);
return ausg;
end;
%%%%%%%%%%%%%%%%% dqe_reduktum %%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% die prozedur dqe_reduktum berechnet das reduktum des diffe-%
% rentialpolynomes bezueglich der variable var . %
% (siehe kapitel 4 abschnitt 4.4) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_reduktum(phi,var);
begin scalar ordc,gradc,hilf,hilfvar,ausg;
ordc := dqe_ord(phi,var);
gradc := dqe_grad(phi,var);
if ordc = 0 then hilfvar := var
else hilfvar := list('d,var,ordc);
hilf := list('expt,hilfvar,gradc);
hilf := reval list('times,dqe_initial(phi,var),hilf);
ausg := reval list('difference,phi,hilf);
return ausg;
end;
%%%%%%%%%%%%%%%%% dqe_separante %%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% die prozedur dqe_separante berechnet die separante eines %
% differentialpolynomes phi bezueglich der variable var . %
% (siehe kapitel 1 definition 1.1.7) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_separante(phi,var);
begin scalar ordc,hilfvar,ausg;
ordc := dqe_ord(phi,var);
if ordc = 0 then hilfvar := var
else hilfvar := list('d,var,ordc);
ausg := dqe_pseudf(phi,hilfvar);
return ausg;
end;
%%%%%%%%%%%%%%%%% dqe_pseudrest %%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%die prozedur dqe_pseudrest berechnet den rest einer pseudo-%
% divition von phi durch psi bezueglich der variable var . %
% (siehe kapitel 4 abschnitt 4.1) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_pseudrest(phi,psi,var);
begin scalar rest, q, k, l, hilf;
rest := phi;
hilf := deg(rest,var);
if not hilf then hilf := 0;
q := 0;
k := 0;
l := deg(psi,var);
if not l then l := 0;
while not(hilf = 0) and not(l = 0) and hilf >= l do
<< k := list('times,reval lcof(rest,var),
list('expt,var,reval list('difference,hilf,l)));
q := list('plus,list('times,reval lcof(psi,var),q),k);
rest :=reval list('difference,reval list('times,lcof(psi,var),rest),
list('times,k,psi));
hilf := deg(rest,var);
if not hilf then hilf := 0 >>;
if not rest then rest := 0
else rest := reval rest;
return rest;
end;
%%%%%%%%%%%%%%%%% dqe_listenord %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
%dqe_listenord ordnet eine liste von differentialpolynomen bzgl.%
% der lexikographischen ordnung der paare, die aus der ordnung %
% und dem grad jedes polynoms bzgl. der variable var bestehen. %
% (siehe kapitel 4 abschnitt 4.7) %
% %
% eingabe : phi von der form list(f1,f2,f3,..,fn) und var. %
% %
% ausgabe : list(f'1,f'2,f'3,...,f'n) wobei %
%(ord f'1,grad f'1)<=(ord f'2,grad f'2)<=...<=(ord f'n,grad f'n)%
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_listenord(phi,var);
begin scalar geordliste,hilflist,hilf,hilf1,erg,testvar;
geordliste := nil;
erg := nil;
testvar := t;
if cdr phi
then
<< hilflist := list(car phi);
phi := cdr phi;
while phi do
<< hilf := car phi;
phi := cdr phi;
while hilflist and testvar do
<< hilf1 := car hilflist;
if dqe_ord(hilf,var) > dqe_ord(hilf1,var)
then
<< erg := dqe_consm(hilf,hilflist);
geordliste := append(geordliste,erg);
testvar := nil >>
else
if dqe_ord(hilf,var) = dqe_ord(hilf1,var) and
dqe_grad(hilf,var) >= dqe_grad(hilf1,var)
then
<< erg := dqe_consm(hilf,hilflist);
geordliste := append(geordliste,erg);
testvar := nil >>
else
<< geordliste := reverse geordliste;
geordliste := reverse dqe_consm(hilf1,geordliste);
hilflist := cdr hilflist >>;
if not(hilflist) and testvar
then geordliste := dqe_modcons(hilf,geordliste)>>;
if phi
then << hilflist := geordliste;
geordliste := nil;
testvar := t >>
else geordliste := reverse geordliste >> >>
else geordliste := phi ;
return geordliste;
end;
%%%%%%%%%%%%%%%% dqe_neqnullfkt %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_neqnullfkt ist hilfsprozedur fuer dqe_elim. %
% (siehe kapitel 4 abschnitt 4.9) %
% %
% eingabe : eine liste phi der form list(elem1,....,elemn). %
% %
% ausgabe : list('or,list('neq,elem1,0),...,list('neq,elmn,0)). %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
procedure dqe_neqnullfkt(phi);
begin scalar r;
if not phi then
return nil;
r := for each elem in phi collect
{'neq,reval elem,0};
if not cdr r then
return car r;
return 'or . r
end;
%%%%%%%%%%%%%%%%%% dqe_equalnullfkt %%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_equalnullfkt ist hilfsprozedur fuer dqe_elim. %
% (siehe kapitel 4 abschnitt 4.9) %
% %
% eingabe : eine liste phi der form list(elem1,....,elemn). %
% %
% ausgabe : list(list('equal,elem1,0),..., %
% list('equal,elmn,0)). %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
procedure dqe_equalnullfkt(phi);
for each elem in phi collect
{'equal,reval elem,0};
%%%%%%%%%%%%%%%% dqe_elimsimplify %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_elimsimplify ist hilfsprozedur fuer dqe_elim. %
% (siehe kapitel 4 abschnitt 4.9) %
% %
% eingabe : phi von der form list(f1,f2,...,fn), zwerg und var. %
% %
% ausgabe : ausg, die aus nzwerg und erg besteht. %
% nzwerg ist die neue zwichenergliste, die aus zwerg %
% und der liste der konstanten polynome bzgl. var %
% gleichgesetzt mit 0. %
% erg ist die liste der differentialpolynome,die nicht%
% konstant bzgl. der variable var sind. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_elimsimplify(phi,zwerg,var);
begin scalar hilfg,hilf,erg1,erg2,ausg;
ausg := nil;
erg1 := nil;
erg2 := nil;
while phi do
<< hilf := car phi;
hilfg := dqe_grad(hilf,var);
if hilfg = 0
then erg1 := dqe_modcons(reval hilf,erg1)
else erg2 := dqe_consm(hilf,erg2) ;
phi := cdr phi >>;
erg1 := dqe_equalnullfkt(erg1);
if erg1
then
<< if not cdr erg1 then erg1 := car erg1
else erg1 := cons('and,erg1)>>;
if zwerg and not cdr zwerg then zwerg := car zwerg;
erg1 := dqe_andorvaleur(list('and,zwerg,erg1));
ausg := list(erg1,erg2);
return ausg;
end;
% part 5
%%%%%%%%%%%%%%%% dqe_start1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% diese prozedur fuehrt die quantorenelimination durch. %
% eingegeben wird nur die eingabeformel. %
% %
% eingabe : eine beliebige formel phi %
% %
% ausgabe : eine positive quantorenfreie formel, die aequi- %
% valent zu phi ist. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_start1(phi);
begin scalar ausg,diffequaliste;
diffequaliste := nil;
if !*dqeverbose
then <<
prin2t "+++++++++++++++++++++++++++++++++++++++++++++++++++++++";
if !*dqeoptsimp then <<
prin2t "+++ dqeoptsimp ist on d.h. die ergebnisse von simplify+";
prin2t "+++ bzw. disjnf bzw. konjnf werden vereinfacht +++">>
else
prin2t "+++ deqoptsimp ist off +++";
if not !*dqegradord then
prin2t "+++ dqegradord ist off +++">>;
if !*dqeoptqelim
then
<<
if !*dqeverbose
then <<
prin2t "+++ das qe_verfahren wird mit aussagenlogischen +++";
prin2t "+++ vereinfachungen ausgefuehrt. +++";
prin2t "+++++++++++++++++++++++++++++++++++++++++++++++++++++++">>;
ausg := dqe_quantelimopt(phi,diffequaliste)
>>
else
<<
if !*dqeverbose
then <<
prin2t "+++ das qe_verfahren wird ohne aussagenlogischen +++";
prin2t "+++ vereinfachungen ausgefuehrt. +++";
prin2t "+++++++++++++++++++++++++++++++++++++++++++++++++++++++">>;
ausg := dqe_quantelim(phi,diffequaliste)
>>;
return ausg;
end;
%%%%%%%%%%%%%%%% dqe_start2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% diese prozedur fuehrt auch wie dqe_start1 die quantoreneli- %
% mination. %
% %
% eingabe : eine beliebige formel phi und %
% eine liste diffequaliste %
% %
% ausgabe : eine positive quantorenfreie formel, die aequi- %
% valent zu phi ist. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_start2(phi,diffequaliste);
begin scalar ausg;
if !*dqeverbose
then <<
prin2t "+++++++++++++++++++++++++++++++++++++++++++++++++++++++";
if !*dqeoptsimp then <<
prin2t "+++ dqeoptsimp ist on d.h. die ergebnisse von simplify+";
prin2t "+++ bzw. disjnf bzw. konjnf werden vereinfacht +++">>
else
prin2t "+++ deqoptsimp ist off +++";
if not !*dqegradord then
prin2t "+++ dqegradord ist off +++"
>>;
if !*dqeoptqelim
then
<<
if !*dqeverbose
then <<
prin2t "+++ das qe_verfahren wird mit aussagenlogischen +++";
prin2t "+++ vereinfachungen ausgefuehrt. +++";
prin2t "+++++++++++++++++++++++++++++++++++++++++++++++++++++++" >>;
ausg := dqe_quantelimopt(phi,diffequaliste)
>>
else
<<
if !*dqeverbose
then <<
prin2t "+++ das qe_verfahren wird ohne aussagenlogischen +++";
prin2t "+++ vereinfachungen ausgefuehrt. +++";
prin2t "+++++++++++++++++++++++++++++++++++++++++++++++++++++++">>;
ausg := dqe_quantelim(phi,diffequaliste);
>>;
return ausg;
end;
%%%%%%%%%%%%%%%% dqe_elim %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% elim ist eine subroutine fuer die prozeduren exqelim und %
% allqelim (siehe abschnitt 5.1 in kapitel 5). %
% %
% eingabe : eine positive quantorenfreie teilformel phi , %
% eine gebundene variable var und diffequaliste . %
% %
% ausgabe : eine positive quantorenfreie formel phi', die %
% aequivalen zu ex var phi ist . %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_elim(phi,diffequaliste,var);
begin scalar hilf,ordhilf,erg1,erg2,ausg,zwerg,phi1,hilfvar,phi2,rest,
hilff,hilfg,ghilf,gradf,gradg,ordf,ordg,redf,initf,const,
erg21,erg22,erg,phi21,phi22,redhilf,sepf,gghilf,liste,helplist;
if !*dqegradord and !*dqeverbose then
prin2t "++++";
zwerg := nil;
phi := dqe_helpelim(phi);
if phi = t or (not phi)
then ausg := phi
else
if not cdr phi
then
<<hilf := car phi;
if !*dqegradord and !*dqeverbose then
<< ordg := dqe_ord(hilf,var);
gradg := dqe_grad(hilf,var);
prin2t "()";
prin2t list(ordg,gradg)
>>;
ausg := dqe_neqnullfkt(dqe_termcoefkt(hilf,var)) >>
else
if car phi = 1 and not cddr phi
then
<<hilf := cadr phi;
if !*dqegradord and !*dqeverbose then
<< ordf := dqe_ord(hilf,var);
gradf := dqe_grad(hilf,var);
prin2t list(ordf,gradf);
prin2t "()"
>>;
erg := dqe_termcoefkt( hilf,var);
hilf := list('equal,reval car erg,0);
erg := dqe_neqnullfkt(cdr erg);
ausg := dqe_andorvaleur(list('or,hilf,erg)) >>
else
<<
hilfg := car phi;
if (dqe_isconstant hilfg) and not(hilfg = 0)
then hilfg := 1;
phi := cdr phi;
ordg := dqe_ord(hilfg,var);
gradg := dqe_grad(hilfg,var);
if not cdr phi
then
<< hilff := car phi;
ordf := dqe_ord(hilff,var);
gradf := dqe_grad(hilff,var);
if !*dqegradord and !*dqeverbose then
<<
prin2t list(ordf,gradf);
prin2t list(ordg,gradg)
>>;
if gradf = 0
then << erg1 := list('equal,reval hilff,0);
erg2 := dqe_neqnullfkt(
dqe_termcoefkt( hilfg,var));
ausg := dqe_andorvaleur(list('and,erg1,erg2)) >>
else
<<redf := dqe_reduktum(hilff,var);
initf := dqe_initial(hilff,var);
if redf = 0
then phi1 := list('and,list('neq,hilfg,0),
list('equal,initf,0))
else
<< phi1 := dqe_equalnullfkt(
dqe_consm(initf,list(redf)));
phi1 :=cons('and,cons(list('neq,hilfg,0),phi1))>>;
if ordf > ordg
then << erg21 := dqe_neqnullfkt(
dqe_termcoefkt(hilfg,var));
erg22 := dqe_neqnullfkt(
dqe_termcoefkt(initf,var));
erg2 :=
dqe_andorvaleur(list('and,erg21,erg22))>>
else
if ordf = ordg
then
<< if ordf = 0 then hilfvar := var
else hilfvar := list('d,var,ordf);
ghilf :=dqe_pseudrest(list('expt,hilfg,gradf),hilff,
hilfvar);
erg21 := dqe_neqnullfkt(dqe_termcoefkt(ghilf,var));
erg22 := dqe_neqnullfkt(dqe_termcoefkt(initf,var));
erg2 := dqe_andorvaleur(list('and,erg21,erg22)) >>
else
<< const := reval list('difference,ordg,ordf);
hilf := dqe_diff(hilff,const,diffequaliste);
hilfvar := list('d,var,ordg);
ghilf := dqe_pseudrest(hilfg,hilf,hilfvar);
if not(dqe_isconstant initf)
then ghilf := reval list('times,initf,ghilf);
phi21 := list('and,list('neq,ghilf,0),
list('equal,hilff,0)) ;
erg21 := dqe_elim(phi21,diffequaliste,var) ;
if dqe_isconstant initf
then gghilf := hilfg
else gghilf :=reval list('times,initf,hilfg);
sepf := dqe_separante(hilff,var);
redhilf := dqe_reduktum(hilf,var);
phi22 := dqe_consm(list('equal,sepf,0),
dqe_consm(list('equal,redhilf,0),
list(list('equal,hilff,0)) ) );
phi22 := cons('and,cons(list('neq,gghilf,0),
phi22));
erg22 := dqe_elim(phi22,diffequaliste,var) ;
erg2 := dqe_andorvaleur(list('or,erg21,erg22))>>;
erg1 := dqe_elim(phi1,diffequaliste,var);
ausg := dqe_andorvaleur(list('or,erg1,erg2)) >> >>
else
<< phi := dqe_elimsimplify(phi,zwerg,var);
zwerg := car phi;
phi := cadr phi;
if not phi
then
<< if !*dqegradord and !*dqeverbose then
<< prin2t "()";
prin2t list(ordg,gradg) >>;
erg := dqe_neqnullfkt(dqe_termcoefkt( hilfg,var));
if zwerg and not cdr zwerg
then ausg :=
dqe_andorvaleur(list('and,erg,car zwerg))
else ausg :=
dqe_andorvaleur(list('and,erg,zwerg)) >>
else
if not cdr phi
then << phi := list('and,list('neq,hilfg,0),
list('equal,car phi,0));
erg := dqe_elim(phi,diffequaliste,var);
if zwerg and not cdr zwerg
then ausg :=
dqe_andorvaleur(list('and,erg,car zwerg))
else
ausg :=dqe_andorvaleur(list('and,erg,zwerg)) >>
else
<<phi := dqe_listenord(phi,var);
if !*dqegradord and !*dqeverbose then
<< liste := phi; helplist := nil;
while liste do
<< hilf := car liste; liste := cdr liste;
helplist := cons( list(dqe_ord(hilf,var),
dqe_grad(hilf,var)),helplist) >>;
prin2t helplist;
prin2t list(ordg,gradg);
>>;
hilff := car phi;
initf := dqe_initial(hilff,var);
redf := dqe_reduktum(hilff,var);
ordf := dqe_ord(hilff,var);
if redf = 0
then
<< phi1 := dqe_equalnullfkt(
dqe_consm(initf,cdr phi));
phi1 := cons('and,cons(list('neq,hilfg,0),phi1))>>
else
<<phi1 := dqe_equalnullfkt(
dqe_consm(initf,dqe_consm(redf,cdr phi)));
phi1 := cons('and,cons(list('neq,hilfg,0),phi1))>>;
if dqe_isconstant initf
then ghilf := hilfg
else ghilf := reval list('times,initf,hilfg);
hilf := cadr phi;
ordhilf := dqe_ord(hilf,var);
if ordhilf = 0
then hilfvar := var
else hilfvar := list('d,var,ordhilf);
if ordhilf = ordf
then rest := dqe_pseudrest(hilf,hilff,hilfvar)
else
<< const := reval list('difference,ordhilf,ordf);
rest := dqe_pseudrest(hilf,dqe_diff(hilff,const,
diffequaliste),hilfvar) >>;
if rest = 0
then phi2 := dqe_equalnullfkt(
dqe_consm(hilff,cddr phi))
else
phi2 := dqe_equalnullfkt(dqe_consm(rest,
dqe_consm(hilff,cddr phi)));
phi2 := cons('and,cons(list('neq,ghilf,0),phi2));
erg1 := dqe_elim(phi1,diffequaliste,var);
erg2 := dqe_elim(phi2,diffequaliste,var);
erg := dqe_andorvaleur(list('or,erg1,erg2));
if zwerg and not cdr zwerg
then ausg := dqe_andorvaleur(list('and,erg,car zwerg))
else ausg :=dqe_andorvaleur(list('and,erg,zwerg)) >> >>
>>;
return ausg;
end;
%%%%%%%%%%%%%%%% dqe_exqelim %%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% exqelim ist eine subroutine fuer die prozedur quantelim %
% (siehe abschnitt 5.2 in kapitel 5). %
% %
% eingabe : eine positive quantorenfreie formel phi, eine ge- %
% bundene variable var und diffequaliste . %
% %
% ausgabe : eine positive quantorenfreie formel phi', die %
% aequivalent zu ex var phi ist . %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_exqelim(phi,diffequaliste,var);
begin scalar hilf,ausg,k,n,timevar,gctimevar,erg;
ausg := nil;n:= 0; k := 0;
if !*dqeverbose then
<<
prin2t "++nun wird ein existenzquantor eliminiert, also muss zuerst";
prin2t "++die formel in disjunktive normalform transformiert werden.";
prin2t "++die disjunktive normalform von ";
mathprint phi;prin2t "++ist :";
>>;
timevar := time();
gctimevar := gctime();
phi := dqe_disjnf(phi);
if !*dqeverbose then
<<
timevar := time() - timevar;
gctimevar := gctime() - gctimevar;
mathprint phi;
prin2 timevar;prin2" ms plus ";prin2 gctimevar;prin2t " ms."
>>;
if (phi = t) or (not phi) then ausg := phi
else
if car phi = 'or
then
<< phi := cdr phi;
if !*dqeverbose then
<<
n := length(phi);
prin2 "++ die anzahl der konjunktionen ist "; prin2t n;
erg := dqe_elimberechnung(phi);
prin2 "++die gesamte anzahl der atomaren formeln ist ";
prin2t car erg;
prin2 "++der ";prin2 cadr erg;
prin2t "_te disjunktionsglied hat die hoechste";
prin2 "++ anzahl von atomaren formeln und zwar ";
prin2t caddr erg;
>>;
while phi do
<< hilf := car phi; k := k + 1;
if !*dqeverbose then
<<
prin2 "++elimination des quantors ex ";
prin2 var; prin2 " vor dem ";
prin2 k;prin2t "-ten konjunktionsglied ";
mathprint hilf;
>>;
timevar := time();
gctimevar := gctime();
hilf := dqe_elim(hilf,diffequaliste,var);
if !*dqeverbose then
<<
timevar := time() - timevar;
gctimevar := gctime() -gctimevar;
prin2 "++die aequivalaente zum ";
prin2 k;prin2t "-ten konjunktionsglied ist : ";
mathprint hilf;
prin2 timevar;prin2" ms plus ";
prin2 gctimevar;prin2t " ms."
>>;
ausg := dqe_modcons(hilf,ausg);
phi := cdr phi >>;
if length(ausg) = 1 then ausg := car ausg
else
if cdr ausg
then ausg := cons('or,ausg) >>
else ausg := dqe_elim(phi,diffequaliste,var);
return ausg;
end;
%%%%%%%%%%%%% dqe_allqelim %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% allqelim ist eine subroutine fuer die prozedur quantelim %
% (siehe abschnitt 5.3 in kapitel 5). %
% %
% eingabe : eine positive quantorenfreie formel phi, eine ge- %
% bundene variable var und diffequaliste . %
% %
% ausgabe : eine positive quantorenfreie formel phi',die %
% aequivalent zu all var phi ist . %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_allqelim(phi,diffequaliste,var);
begin scalar hilf,ausgb,k,n,timevar,gctimevar,erg;
ausgb := nil;n := 0; k := 0;
if !*dqeverbose
then
<<
prin2t "++nun wird ein allquantor eliminiert, also muss zuerst ";
prin2t "++die formel in konjunktive normalform transformiert werden. ";
prin2t "++die konjunktive normalform von ";
mathprint phi;prin2t "ist :";
>>;
timevar := time();
gctimevar := gctime();
phi := dqe_konjnf(phi);
if !*dqeverbose
then
<<
timevar := time() - timevar;
gctimevar := gctime() - gctimevar;
mathprint phi;
prin2 timevar;prin2" ms plus ";prin2 gctimevar;prin2t " ms."
>>;
if (phi = t) or (not phi)
then ausgb := phi
else
if car phi = 'and
then
<<phi := cdr phi;
n := length(phi);
if !*dqeverbose then
<<
prin2 "++die anzahl der disjunktionen ist "; prin2t n;
erg := dqe_elimberechnung(phi);
prin2 "++die gesamte anzahl der atomaren formeln ist ";
prin2t car erg;
prin2 "++der ";prin2 cadr erg;
prin2t "_te disjunktionsglied hat die hoechste";
prin2 " anzahl von atomaren formeln und zwar ";prin2t caddr erg;
>>;
while phi do
<<hilf := car phi;k := k + 1;
if !*dqeverbose then
<<
prin2 "++elimination des quantors all ";
prin2 var; prin2 " vor dem ";
prin2 k;prin2t "-ten disjunktionsglied ";
mathprint hilf;
>>;
timevar := time();
gctimevar := gctime();
hilf := dqe_makepositive list('nott,hilf);
hilf := dqe_elim(hilf,diffequaliste,var);
hilf := dqe_makepositive list('nott,hilf);
if !*dqeverbose then
<<
timevar := time() - timevar;
gctimevar := gctime() - gctimevar;
prin2 "++die aequivalaente zum ";
prin2 k;prin2t "-ten disjunktionsglied ist : ";
mathprint hilf;
prin2 timevar;prin2" ms plus ";
prin2 gctimevar;prin2t " ms."
>>;
ausgb := dqe_modcons(hilf,ausgb);
phi := cdr phi >>;
if length(ausgb) = 1
then ausgb := car ausgb
else
if cdr ausgb
then ausgb := cons('and,ausgb) >>
else
<< phi := dqe_makepositive list('nott,phi);
ausgb := dqe_elim(phi,diffequaliste,var) ;
ausgb := dqe_makepositive list('nott,ausgb) >>;
return ausgb;
end;
%%%%%%%%%%%%%%%%%% dqe_quantelim %%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% quantelim ist die hauptprozedur fuer quantorenelimination %
% (siehe abschnitt 5.4 des kapitels 5). %
% %
% eingabe : eine beliebige formel phi . %
% ausgabe : eine positive quantorenfreie formel phi', die %
% aequivalent zu phi ist. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_quantelim(phi,diffequaliste);
begin scalar hilf,liste,var,erg,quant,n,k,timevar,gctimevar;
liste := nil;
erg := nil;
n := 0;
timevar := time();
gctimevar := gctime();
phi := dqe_makepositive phi;
if not dqe_isprenexp phi
then
<< if not diffequaliste
then phi := dqe_makeprenex phi
else << hilf := dqe_makeprenexmod(phi,diffequaliste);
phi := car hilf;
diffequaliste := cadr hilf >> >>;
if !*dqeverbose then
<<
timevar := time() - timevar;
gctimevar := gctime() - gctimevar;
prin2t "+++die praenexe form der eingabeformel ist";
mathprint phi;
prin2 timevar;prin2" ms plus ";prin2 gctimevar;prin2t " ms.";
>>;
while car phi = 'ex or car phi = 'all do
<< hilf := list(car phi,cadr phi);
liste := cons(hilf,liste);
n := n + 1;
phi := caddr phi >>;
if !*dqeverbose then
<<
prin2t "+++die matrix der eingabeformel ist";
mathprint phi;
>>;
erg := phi;
if !*dqeverbose then
<<
prin2 "+++die anzahl der quantoren ist ";mathprint n;
>>;
if n = 0 then
<<
if !*dqeverbose then
prin2t "+++die eingabeformel ist quantorenfrei" >>
else
if n = 1
then
<< hilf := car liste;
liste := cdr liste;
quant := car hilf;
var := cadr hilf;
if !*dqeverbose then
<<
prin2 "+++es gibt nur den quantor ";
prin2 quant;prin2 ",";prin2 var;
prin2t " zu eliminieren.";
>>;
if quant = 'ex
then erg := dqe_exqelim(erg,diffequaliste,var)
else erg := dqe_allqelim(erg,diffequaliste,var)
>>
else
<< k := 0;
if !*dqeverbose then
<<
prin2 "es gibt ";prin2 n;
prin2t " quantoren zu eliminieren.";
>>;
while liste do
<< hilf := car liste;
liste := cdr liste;
quant := car hilf;
var := cadr hilf;
k := k + 1;
if !*dqeverbose then
<<
prin2 " elimination des "; prin2 k;prin2 "-ten quantors ";
prin2 quant; prin2t var
>>;
timevar := time();
gctimevar := gctime();
if quant = 'ex
then erg := dqe_exqelim(erg,diffequaliste,var)
else erg := dqe_allqelim(erg,diffequaliste,var);
if !*dqeverbose then
<<
timevar := time() - timevar;
gctimevar := gctime() - gctimevar;
prin2 "nach der elimination des ";
prin2 k;prin2t "-ten quantors";
prin2t "sieht die quantorenfreie formel, wie folgt, aus: ";
mathprint erg;
prin2 timevar;prin2" ms plus ";
prin2 gctimevar;prin2t " ms.";
>>;
>> >>;
if !*dqeverbose then
prin2t "+++die aequivalaente quantorenfreie formel ist+++: ";
return erg;
end;
%%%%%%%%%%%%%%%%%% dqe_elimopt %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% elimopt ist eine subroutine der prozeduren exqelimopt und %
% allqelimopt. sie arbeitet wie elim aber sie verwendet die %
% hilfsprozedur simplify (siehe abschnitt 5.5 des kapitels 5).%
% %
% eingabe : eine positive quantorenfreie teilformel phi , %
% eine gebundene variable var und diffequaliste . %
% %
% ausgabe : eine vereinfachte positive quantorenfreie formel %
% phi', die aequivalen zu ex var phi ist . %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_elimopt(phi,diffequaliste,var);
begin scalar nf;
if !*dqegradord and !*dqeverbose then
prin2t "++++";
nf := dqe_helpelim phi;
if (nf = t) or (not nf) then
return nf;
if not cdr nf then
return dqe_elimopt!-neq(nf,diffequaliste,var);
if car nf = 1 and not cddr nf then
return dqe_elimopt!-oneeq(nf,diffequaliste,var);
return dqe_elimopt!-regular(nf,diffequaliste,var)
end;
procedure dqe_elimopt!-neq(phi,diffequaliste,var);
begin scalar res,prod,ordg,gradg;
prod := car phi;
if !*dqegradord and !*dqeverbose then <<
ordg := dqe_ord(prod,var);
gradg := dqe_grad(prod,var);
prin2t "()";
prin2t {ordg,gradg};
>>;
res := dqe_neqnullfkt dqe_termcoefkt(prod,var);
res := dqe_simplify res
return res
end;
procedure dqe_elimopt!-oneeq(phi,diffequaliste,var);
begin scalar equ,ordf,gradf,erg,res;
equ := cadr phi;
if !*dqegradord and !*dqeverbose then <<
ordf := dqe_ord(equ,var);
gradf := dqe_grad(equ,var);
prin2t list(ordf,gradf);
prin2t "()";
>>;
erg := dqe_termcoefkt( equ,var);
equ := dqe_simplify {'equal,reval car erg,0}; % Warning: Must return eq
if equ = T then
return T;
erg := cdr erg;
erg := dqe_neqnullfkt erg ;
res := dqe_andorvaleur {'or,equ,erg};
res := dqe_simplify res;
return res
end;
procedure dqe_elimopt!-regular(phi,diffequaliste,var);
begin scalar g,eqs;
g := car phi;
eqs := cdr phi;
if (dqe_isconstant g) and not(g = 0) then
g := 1;
if not cdr eqs then
return dqe_elimopt!-regular!-oneeq(g,eqs,diffequaliste,var);
return dqe_elimopt!-regular1(g,eqs,diffequaliste,var);
end;
procedure dqe_elimopt!-regular1(g,eqs,diffequaliste,var);
begin scalar eqs,hilf,ordhilf,erg1,erg2,ausg,zwerg,phi1,hilfvar,phi2,rest;
scalar hilff,g,ghilf,gradg,ordf,ordg,redf,initf,const;
scalar erg,weiter;
scalar liste, helplist,phi;
ordg := dqe_ord(g,var);
gradg := dqe_grad(g,var);
phi := dqe_elimsimplify(eqs,zwerg,var);
zwerg := car phi; phi := cadr phi;
if not zwerg then
weiter := t
else <<
if not cdr zwerg then
zwerg := dqe_simplify car zwerg
else
zwerg := dqe_simplify zwerg;
if zwerg = nil then
weiter := nil
else weiter := t
>>;
if weiter = nil then
ausg := nil
else <<
if not phi then <<
if !*dqegradord and !*dqeverbose then <<
prin2t "()";
prin2t list(ordg,gradg)
>>;
erg := dqe_neqnullfkt(dqe_termcoefkt( g,var));
if zwerg = t then
ausg := erg
else ausg := dqe_andorvaleur(
list('and,erg,zwerg));
ausg := dqe_simplify ausg
>> else if not cdr phi then <<
phi := list('and,list('neq,g,0),
list('equal,car phi,0));
erg := dqe_elimopt(phi,diffequaliste,var);
if zwerg = t then
ausg := erg
else if erg = t then <<
if not zwerg then
ausg := t
else
ausg := zwerg
>> else
ausg := dqe_andorvaleur(
list('and,erg,zwerg));
ausg := dqe_simplify ausg
>> else <<
phi := dqe_listenord(phi,var);
if !*dqegradord and !*dqeverbose then <<
liste := phi; helplist := nil;
while liste do <<
hilf := car liste; liste := cdr liste;
helplist := cons( list(dqe_ord(hilf,var),
dqe_grad(hilf,var)),
helplist)
>>;
prin2t helplist;
prin2t list(ordg,gradg);
>>;
hilff := car phi;
initf := dqe_initial(hilff,var);
redf := dqe_reduktum(hilff,var);
ordf := dqe_ord(hilff,var);
if redf = 0 then
phi1 := dqe_equalnullfkt(dqe_consm(initf,cdr phi))
else
phi1 := dqe_equalnullfkt(dqe_consm(initf,
dqe_consm(redf,cdr phi)));
phi1 := cons('and,cons(list('neq,g,0),phi1));
if dqe_isconstant initf then
ghilf := g
else
ghilf := reval list('times,initf,g);
hilf := cadr phi;
ordhilf := dqe_ord(hilf,var);
if ordhilf = 0 then
hilfvar := var
else
hilfvar := list('d,var,ordhilf);
if ordhilf = ordf then
rest := dqe_pseudrest(hilf,hilff,hilfvar)
else <<
const := reval list('difference,ordhilf,ordf);
rest :=dqe_pseudrest(hilf,dqe_diff(hilff,const,
diffequaliste),hilfvar)
>>;
if rest = 0 then
phi2 := dqe_equalnullfkt(
dqe_consm(hilff,cddr phi))
else
phi2 := dqe_equalnullfkt(dqe_consm(rest,
dqe_consm(hilff,cddr phi)));
phi2 := cons('and,cons(list('neq,ghilf,0),phi2));
erg2 := dqe_elimopt(phi2,diffequaliste,var);
if erg2 = t then
erg := t
else <<
erg1 := dqe_elimopt(phi1,diffequaliste,var);
if erg1 = t then
erg := t
else
erg := dqe_andorvaleur(list('or,erg1,erg2))
>>;
if zwerg = t then
ausg := erg
else if erg = t then <<
if not zwerg then
ausg := t
else
ausg := zwerg
>> else
ausg :=dqe_andorvaleur(list('and,erg,zwerg)) ;
ausg := dqe_simplify ausg
>>
>>;
return ausg;
end;
procedure dqe_elimopt!-regular!-oneeq(g,eqs,diffequaliste,var);
begin scalar eqs,hilf,erg1,erg2,ausg,phi1,hilfvar;
scalar hilff,g,ghilf,gradf,gradg,ordf,ordg,redf,initf,const;
scalar erg21,erg22,phi21,phi22,redhilf,sepf,gghilf;
ordg := dqe_ord(g,var);
gradg := dqe_grad(g,var);
hilff := car eqs;
gradf := dqe_grad(hilff,var);
ordf := dqe_ord(hilff,var);
if !*dqegradord and !*dqeverbose then <<
prin2t {ordf,gradf};
prin2t {ordg,gradg};
>>;
if gradf = 0 then <<
erg1 := dqe_simplify list('equal,reval hilff,0);
if erg1 = nil then
ausg := nil
else <<
erg2 := dqe_neqnullfkt(dqe_termcoefkt( g,var));
if erg1 = t then
ausg := erg2
else
ausg := dqe_andorvaleur(list('and,erg1,erg2)) ;
ausg := dqe_simplify ausg
>>
>> else <<
redf := dqe_reduktum(hilff,var);
initf := dqe_initial(hilff,var);
if redf = 0 then
phi1 := list('and,list('neq,g,0)
, list('equal,initf,0))
else <<
phi1 :=dqe_equalnullfkt(dqe_consm(initf,list(redf)));
phi1 := cons('and,cons(list('neq,g,0),phi1))
>>;
if ordf > ordg then <<
erg21 := dqe_neqnullfkt(
dqe_termcoefkt(g,var));
erg22 := dqe_neqnullfkt(
dqe_termcoefkt(initf,var));
erg2 := dqe_simplify
dqe_andorvaleur(list('and,erg21,erg22))
>> else if ordf = ordg then <<
if ordf = 0 then
hilfvar := var
else
hilfvar := list('d,var,ordf);
ghilf :=dqe_pseudrest(list('expt,g,gradf),hilff,
hilfvar);
erg21 := dqe_neqnullfkt(dqe_termcoefkt(ghilf,var));
erg22 := dqe_neqnullfkt(dqe_termcoefkt(initf,var));
erg2 := dqe_simplify
dqe_andorvaleur(list('and,erg21,erg22))
>> else <<
const := reval list('difference,ordg,ordf);
hilf := dqe_diff(hilff,const,diffequaliste);
hilfvar := list('d,var,ordg);
ghilf := dqe_pseudrest(g,hilf,hilfvar);
if not(dqe_isconstant initf) then
ghilf := reval list('times,initf,ghilf);
phi21 := list('and,list('neq,ghilf,0),
list('equal,hilff,0));
erg21 := dqe_elimopt(phi21,diffequaliste,var) ;
if erg21 = t then
erg2 := erg21
else << if dqe_isconstant initf then
gghilf := g
else gghilf :=
reval list('times,initf,g);
sepf := dqe_separante(hilff,var);
redhilf := dqe_reduktum(hilf,var);
phi22 := dqe_consm(list('equal,sepf,0),
dqe_consm(list('equal,redhilf,0),
list(list('equal,hilff,0)) ) );
phi22 := cons('and,cons(list('neq,gghilf,0),
phi22));
erg22 := dqe_elimopt(phi22,diffequaliste,var) ;
erg2 := dqe_andorvaleur(list('or,erg21,erg22))
>>
>>;
if erg2 = t then
ausg := t
else <<
erg1 := dqe_elimopt(phi1,diffequaliste,var);
if erg1 = t then
ausg := t
else
ausg := dqe_andorvaleur(list('or,erg1,erg2));
ausg := dqe_simplify ausg >>
>>;
return ausg;
end;
%%%%%%%%%%%%%%%%% dqe_exqelimopt %%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% exqelimopt ist eine subroutine fuer quantelimopt. sie ar- %
% beitet wie exqelim (siehe abschnitt 5.5). %
% %
% eingabe : eine positive quantorenfreie formel phi, eine ge- %
% junktiver nomalform , eine gebundene variable var %
% bundene variable var und diffequaliste . %
% %
% ausgabe : eine vereinfachte positive quantorenfreie formel %
% phi', die aequivalent zu ex var phi ist . %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_exqelimopt(phi,diffequaliste,var);
begin scalar hilf,erg,testvar,k,n,timevar,gctimevar,ausg;
erg := nil; testvar := t; n := 0; k := 0;
if !*dqeverbose
then
<<
prin2t "++nun wird ein existenzquantor eliminiert, also muss zuerst ";
prin2t "++die formel in disjunktive normalform transformiert werden. ";
prin2t "++die disjunktive normalform von ";
mathprint phi; prin2t " ist";
>>;
timevar := time();
gctimevar := gctime();
phi := dqe_disjnf(phi);
if !*dqeverbose
then
<<
timevar := time() - timevar;
gctimevar := gctime() - gctimevar;
mathprint phi;
prin2 timevar; prin2 " ms plus ";prin2 gctimevar;prin2t " ms."
>>;
if (phi = t) or not(phi) then erg := phi
else
if car phi = 'or
then
<< phi := cdr phi; testvar := t;
if !*dqeverbose then
<<
n := length(phi);
prin2 "++die anzahl der konjunktionen ist "; prin2t n;
ausg := dqe_elimberechnung(phi);
prin2 "++die gesamte anzahl der atomaren formeln ist ";
prin2t car ausg;
prin2 "++der ";prin2 cadr ausg;
prin2t "_te disjunktionsglied hat die
hoechste";
prin2 " ++anzahl von atomaren formeln und zwar ";
prin2t caddr ausg;
>>;
while phi and testvar do
<< hilf := car phi; k := k + 1;
if !*dqeverbose then
<<
prin2 "++elimination des quantors ex";prin2 ",";
prin2 var; prin2 " vor dem ";
prin2 k; prin2t "-ten konjunktionsglied ";
mathprint hilf;
>>;
timevar := time();
gctimevar := gctime();
hilf := dqe_elimopt(hilf,diffequaliste,var);
if !*dqeverbose then
<<
timevar := time() - timevar;
gctimevar := gctime() - gctimevar;
prin2 "++ die aequivalaente zum ";
prin2 k; prin2t "-ten konjunktionsglied ist :";
mathprint hilf;
prin2 timevar;prin2 " ms plus ";
prin2 gctimevar;prin2t " ms."
>>;
if hilf = t
then testvar := nil
else erg := dqe_consm(hilf,erg);
phi := cdr phi >>;
if not(testvar) then erg := t
else
if length(erg) = 1 then erg := dqe_simplify car erg
else
if cdr erg
then erg := dqe_simplify
cons('or,reverse erg) >>
else erg := dqe_elimopt(phi,diffequaliste,var);
return erg;
end;
%%%%%%%%%%%%%%%%% dqe_allqelimopt %%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% allqelimopt ist eine subroutine fuer quantelimopt. sie ar- %
% beitet wie allqelim (siehe abschnitt 5.5). %
% %
% eingabe : eine positive quantorenfreie formel phi, eine ge- %
% junktiver nomalform , eine gebundene variable var %
% bundene variable var und diffequaliste . %
% %
% ausgabe : eine vereinfachte positive quantorenfreie formel %
% phi', die aequivalent zu all var phi ist . %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_allqelimopt(phi,diffequaliste,var);
begin scalar hilf,erg,testvar,k,n,timevar,gctimevar,ausg;
erg := nil; testvar := t; k := 0;
if !*dqeverbose
then
<<
prin2t "++nun wird ein allquantor eliminiert, also muss zuerst ";
prin2t "++die formel in konjunktive normalform transformiert werden. ";
prin2t "++die konjunktive normalform von ";
mathprint phi;prin2t "ist:"
>>;
timevar := time();
gctimevar := gctime();
phi := dqe_konjnf(phi);
if !*dqeverbose
then
<<
timevar := time() - timevar;
gctimevar := gctime() - gctimevar;
mathprint phi;
prin2 timevar; prin2 " ms plus ";prin2 gctimevar;prin2t " ms."
>>;
if (phi = t) or not(phi) then erg := phi
else
if car phi = 'and
then
<< phi := cdr phi; k := 0;
n := length(phi);
if !*dqeverbose
then
<<
prin2 "++ die anzahl der disjunktionen ist "; prin2t n;
ausg := dqe_elimberechnung(phi);
prin2 "++die gesamte anzahl der atomaren formeln ist ";
prin2t car ausg;
prin2 "++der ";prin2 cadr ausg;
prin2t "_te disjunktionsglied hat die hoechste";
prin2 " anzahl von atomaren formeln und zwar ";
prin2t caddr ausg;
>>;
while phi and testvar do
<<hilf := car phi; k := k + 1;
if !*dqeverbose then
<<
prin2 "elimination des quantors all ";prin2 ",";
prin2 var; prin2 " vor dem ";
prin2 k; prin2t "-ten disjunktionsglied ";
mathprint hilf;
>>;
timevar := time();
gctimevar := gctime();
hilf := dqe_makepositive list('nott,car phi);
hilf := dqe_elimopt(hilf,diffequaliste,var);
hilf := dqe_makepositive list('nott,hilf);
if !*dqeverbose then
<<
timevar := time() - timevar;
gctimevar := gctime() - gctimevar;
prin2 "++ die aequivalaente zum ";
prin2 k; prin2t "-ten disjunktionsglied ist :";
mathprint hilf;
prin2 timevar;prin2 " ms plus ";
prin2 gctimevar;prin2t " ms."
>>;
if hilf = nil
then testvar := nil
else erg := dqe_consm(hilf,erg);
phi := cdr phi >>;
if not(testvar) then erg := nil
else
if length(erg) = 1 then erg := dqe_simplify car erg
else
if cdr erg
then erg := dqe_simplify
cons('and,reverse erg) >>
else
<< phi := dqe_makepositive list('nott,phi);
erg := dqe_elimopt(phi,diffequaliste,var) ;
erg := dqe_makepositive list('nott,erg) >>;
return erg;
end;
%%%%%%%%%%%%%%%%%%%% dqe_quantelimopt %%%%%%%%%%%%%%%%%%%%%%%%%
% %
% quantelimopt ist wie quantelim eine hauptprozedur fuer quant-%
% orenelimination mit aussagenlogischen vereinfachungen (siehe %
% abschnitt 5.5 des kapitels 5). %
% %
% eingabe : eine beliebige formel phi . %
% ausgabe : eine vereinfachte positive quantorenfreie formel %
% phi', die aequivalent zu phi ist. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_quantelimopt(phi,diffequaliste);
begin scalar hilf,liste,var,ausg,quant,weiter,k,n,timevar,gctimevar;
weiter := t;
n := 0;
liste := nil;
ausg := nil;
timevar := time();
gctimevar := gctime();
phi := dqe_makepositive phi;
if not dqe_isprenexp phi
then
<< if not diffequaliste
then phi := dqe_makeprenex phi
else << hilf := dqe_makeprenexmod(phi,diffequaliste);
phi := car hilf;
diffequaliste := cadr hilf >> >>;
if !*dqeverbose then
<<
timevar := time() - timevar;
gctimevar := gctime() - gctimevar;
prin2t "+++die praenexe form der eingabeformel ist";
mathprint phi;
prin2 timevar;prin2" ms plus ";
prin2 gctimevar;prin2t " ms.";
>>;
while car phi = 'ex or car phi = 'all do
<< hilf := list(car phi,cadr phi);
liste := cons(hilf,liste);
n := n + 1;
phi := caddr phi >>;
if !*dqeverbose then
<<
prin2t "+++die matrix der eingabeformel ist";
mathprint phi;
>>;
ausg := phi;
if !*dqeverbose then
<< prin2 "+++die anzahl der quantoren ist ";mathprint n >>;
if n = 0 then
<<
if !*dqeverbose then
prin2t "+++die eingabeformel ist quantorenfrei" >>
else
if n = 1 then
<< hilf := car liste;
liste := cdr liste;
quant := car hilf;
var := cadr hilf;
if !*dqeverbose then
<<
prin2 "+++es gibt nur den quantor ";
prin2 quant;prin2",";prin2 var;
prin2t " zu eliminieren.";
>>;
if quant = 'ex
then ausg := dqe_exqelimopt(ausg,diffequaliste,var)
else ausg := dqe_allqelimopt(ausg,diffequaliste,var) ;
>>
else
<< k := 0;
if !*dqeverbose then
<<
prin2 "+++es gibt ";prin2 n;
prin2t " quantoren zu eliminieren.";
>>;
while liste and weiter do
<< hilf := car liste;
liste := cdr liste;
quant := car hilf;
var := cadr hilf;
k := k + 1;
if !*dqeverbose
then
<<
prin2 " elimination des ";
prin2 k;prin2 "-ten quantors ";
prin2 quant; prin2t var ;
>>;
timevar := time();
gctimevar := gctime();
if quant = 'ex
then ausg := dqe_exqelimopt(ausg,diffequaliste,var)
else ausg := dqe_allqelimopt(ausg,diffequaliste,var);
if !*dqeverbose then
<<
timevar := time() - timevar;
gctimevar := gctime() - gctimevar;
prin2 "+++nach der elimination des ";
prin2 k;prin2t "-ten quantors";
prin2t "sieht die quantorenfreie formel, wie folgt, aus: ";
mathprint ausg;
prin2 timevar;prin2" ms plus ";
prin2 gctimevar;prin2t " ms.";
>>;
if (ausg = t) or not(ausg)
then weiter := nil >> >>;
if !*dqeverbose then
prin2t "+++die aequivalaente vereinfachte quantorenfreie formel ist: ";
return ausg;
end;
% part 6
%%%%%%%%%%%%%%% dqe_elimberechnung %%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% diese prozedur berechnet die anzahl der atomaren formeln in %
% einer positiven quantorenfreien formel, die in disjunktiver %
% bzw. konjunktiver normalform ist. ausserdem bestimmt sie %
% den laengesten konjunktions- bzw. disjunktionsglied. %
% %
% eingabe: eine positive quantorenfreie formel phi, die in dis- %
% junktiver bzw. konjunktiver normalform ist. %
% %
% ausgabe: eine liste,die aus erg1, erg2 und erg3 besteht. %
% erg1 ist anzahl der atomaren formeln in phi. %
% erg2 ist der index des in phi vorkommenden laengen %
% gliedes und erg3 ist die anzahl der atomaren formeln %
% dieses gliedes. %
% sie wird von ex- bzw. allqelim und ex- bzw. allqelimopt %
% aufgerufen. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_elimberechnung(phi);
begin scalar erg,erg1,erg2,erg3,hilf,k;
if phi = t or not phi
or dqe_isatomarp(phi)
then
<< erg1 := 1; erg2 := 1; erg3 := 1>>
else
<< erg1 := 0; erg2 := 0; erg3 := 0; k := 0;
phi := cdr phi;
while phi do
<< k := k + 1;
hilf := car phi; phi := cdr phi;
hilf := dqe_elimberechnung(hilf);
erg1 := erg1 + car hilf;
if car hilf > erg3
then
<< erg2 := k; erg3 := car hilf>> >> >>;
erg := list(erg1,erg2,erg3);
return erg;
end;
%%%%%%%%%%%%% dqe_helpsimplify %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_helpsimplify ist eine hilfsprozedur fuer dqe_simplify. %
% sie transformiert jede positive quantorenfreie formel zuerst %
% in disjuntive normalform. dann fuehrt sie die folgende ver- %
% einfachungen durch : %
% 1 fall : die formel von der form (a = 0 and ... and a neq 0) %
% wird zu false vereinfacht. %
% %
% 2 fall : die formel von der form (a = 0 or ... or a neq 0) %
% wird zu true vereinfacht. %
% %
% 3 fall : die formel von der form (phi and a = 0) or ... or psi%
% or (phi and a neq 0) wird mit hilfe der prozedur %
% dqe_logsimp zu phi or ... or psi vereinfacht. %
% 4 fall : die formel von der form (phi and a = 0) or ... or psi%
% or a = 0 wird zu a = 0 or ...or psi (analog fuer %
% a neq 0) vereinfacht. %
% sie wird von simplify aufgerufen. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_helpsimplify(phi);
begin scalar ausg,hilf,hilfphi,liste1,liste2,weiter;
scalar aliste,kliste;
ausg := nil;
if phi = t or not phi or dqe_isatomarp(phi)
then ausg := phi
else
<< phi := dqe_disjnf(phi);
if car phi = 'and
then
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% hier wird a = 0 and ... and a neq 0 zu fasle vereinfacht%
% phi wird in zwei listen aufgeteilt. liste2 enthaelt die %
% atomare formeln mit gleichung und liste1 enthaelt die %
% atom. formeln mit ungl. . falls ein element der liste1 %
% aus der liste2 ist, dann ist die ausgabe nil. sonst phi.%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
<< hilfphi := cdr phi; liste1 := nil; liste2 := nil;
while hilfphi do
<< hilf := car hilfphi; hilfphi := cdr hilfphi;
if car hilf = 'neq
then liste1 := dqe_consm(hilf,liste1)
else liste2 := dqe_consm(hilf,liste2) >>;
weiter := t;
while liste1 and weiter do
<< hilf := car liste1; liste1 := cdr liste1;
hilf := dqe_makepositive list('nott,hilf);
if hilf member liste2
then weiter := nil >>;
if not weiter
then ausg := nil
else ausg := phi >>
else
<< hilfphi := cdr phi; weiter := t; aliste := nil;
kliste := nil;
while hilfphi and weiter do
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% hier wird phi in zwei listen aufgeteilt. %
% aliste enthaelt nur die atomaren formeln. %
% kliste enthaelt die konjunktionen. %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
<< hilf := car hilfphi; hilfphi := cdr hilfphi;
hilf := dqe_helpsimplify(hilf);
if hilf = t then weiter := nil
else
if dqe_isatomarp hilf
then aliste := dqe_modcons(hilf,aliste)
else
if hilf
then kliste := dqe_modcons(hilf,kliste)>>;
if kliste
then
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% hier wird a = 0 or psi and a = 0 zu psi vereinfacht. %
% falls ein element der aliste in einem element der kliste%
% vorkommt,dann wird dieses element aus der aliste enfernt%
% statt a = 0 and psi nur psi kommt in kliste. %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
<<liste1 := aliste;
while liste1 do
<<liste2 := kliste;
hilf := car liste1;liste1 := cdr liste1;
while liste2 do
<< if hilf member car liste2
then kliste := dqe_sanselem(car liste2,
kliste);
liste2 := cdr liste2 >> >> >>;
if not weiter then ausg := t
else
<< hilfphi := aliste;
if length(aliste) = 1
then aliste := car aliste
else
if aliste
then aliste := cons('or,aliste);
liste1 := nil; liste2 := nil;
while hilfphi do
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% hier wird a = 0 or ... or a neq 0 zu true vereinfacht.%
% hilfphi wird in zwei listen aufgeteilt. liste2 enthaelt %
% atomare formeln mit gleichung und liste1 enthaelt die %
% atom. formeln mit ungl. . falls ein element der liste1 %
% aus der liste2 ist,dann ist die ausgabe t. sonst hilfphi%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
<<hilf := car hilfphi; hilfphi := cdr hilfphi;
if car hilf = 'neq
then liste1 := dqe_consm(hilf,liste1)
else liste2 := dqe_consm(hilf,liste2) >>;
weiter := t;
while liste1 and weiter do
<<hilf := car liste1; liste1 := cdr liste1;
hilf := dqe_makepositive list('nott,hilf);
if hilf member liste2
then weiter := nil >>;
if not weiter then ausg := t
else
if not kliste
then ausg := aliste
else
if not cdr kliste
then ausg := dqe_andorvaleur list('or,
aliste,car kliste)
else
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% mit hilfe deq_logsimp wird a = 0 and psi or a neq 0 and %
% psi zu psi vereinfacht. %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
<< hilfphi := dqe_logsimp(kliste);
if not hilfphi
then ausg := aliste
else
if dqe_isatomarp hilfphi
then
<< if not aliste
then ausg := hilfphi
else
<<if dqe_isatomarp aliste
then ausg := list('or,
aliste,hilfphi)
else ausg := dqe_modcons
(hilfphi,aliste);
ausg := dqe_helpsimplify(phi) >>>>
else
if car hilfphi ='and
then ausg := dqe_andorvaleur list('or,
aliste,hilfphi)
else
<<ausg := dqe_andorvaleur list('or,
aliste,hilfphi);
if not(cdr hilfphi = kliste)
then ausg := dqe_helpsimplify(ausg)
>>
>> >> >> >>;
return ausg;
end;
%%%%%%%%%%%%%%% dqe_logsimp %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_logsimp ist eine hilfsprozedur von dqe_helpsimplify. mit %
% hilfe dieser prozedur wird jede positive quantorenfreie formel%
% von der form (phi and a = 0) or... or psi or (phi and a neq 0)%
% zu phi or ... or psi vereinfacht. %
% %
% eingabe : eine liste von konjunktionen. %
% %
% ausgabe : eine liste von konjunktionen mit oben beschriebenen %
% vereinfachung. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_logsimp(phi);
begin scalar konjlist,erg,hilf,aliste,liste,weiter,hilfphi;
scalar constant,hilff;
erg := nil; liste := nil;
hilfphi := phi;
while hilfphi do
<< konjlist := cdar hilfphi;constant := car hilfphi;
hilfphi := cdr hilfphi;
liste := hilfphi;
aliste := nil;
while konjlist do
<< hilf := car konjlist; konjlist := cdr konjlist;
hilff := dqe_makepositive list('nott,hilf);
weiter := t;
while liste and weiter do
<< if hilff member car liste
and
dqe_listequal( dqe_sanselem(car liste,hilff),
dqe_sanselem(constant,hilf) )
then weiter := nil
else liste := cdr liste >>;
if weiter
then
aliste := dqe_consm(hilf,aliste)
else
hilfphi := dqe_sanselem(hilfphi,car liste) ;
liste := hilfphi >>;
if length aliste = 1
then erg := dqe_consm(car aliste,erg)
else
if aliste
then erg := dqe_consm(cons('and,reverse aliste),erg) >>;
if length erg = 1 then erg := car erg
else
if erg then erg := cons('or,reverse erg);
return erg;
end;
%%%%%%%%%%%%%%% dqe_listequal %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_listequal testet ob zwei listen die selben elemente haben.%
% %
% eingabe : zwei listen. %
% %
% ausgabe : true falls diese listen dieselbe menge darstellen %
% false sonst %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_listequal(phi,psi);
begin scalar ausg,weiter;
ausg := nil; weiter := t;
if not(length phi = length psi)
then ausg := nil
else
<< while phi and weiter do
<< if car phi member psi
then phi := cdr phi
else weiter := nil >>;
if weiter then ausg := t
else ausg := nil >>;
return ausg;
end;
%%%%%%%%%%%%%%% dqe_vorkommen %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_vorkommen berechnet,wie oft die atomare formel der form %
% (elem = 0) oder not(elem = 0) in einer positiven quantoren- %
% quantorenfreien formel phi vorkommt. %
% (siehe abschnitt 6.1 des kapitels 6) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_vorkommen(elem,phi);
begin scalar erg,hilf;
if phi = t or not phi then erg := 0
else
if car phi = 'neq or car phi = 'equal
then
<< if cadr phi = elem then erg := 1
else erg := 0>>
else
<< phi := cdr phi;
while phi do
<< hilf := dqe_vorkommen(elem,car phi);
erg := erg + hilf;
phi := cdr phi >> >>;
return erg;
end;
%%%%%%%%%%%%% dqe_laengefkt %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_laengefkt bestimmt die anzahl der atomaren formeln einer %
% positiven quantorenfreien formel phi. %
% (siehe abschnitt 6.1 des kapitels 6) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_laengefkt(phi);
begin scalar erg,hilf;
erg := 0;
if phi = t or not phi then erg := 0
else
if car phi = 'equal or car phi = 'neq
then erg := 1
else
<< phi := cdr phi;
while phi do
<< hilf := dqe_laengefkt(car phi);
erg := erg + hilf;
phi := cdr phi >> >>;
return erg;
end;
%%%%%%%%%%%%%%% dqe_specneq %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_specneq ist eine hilfsprozedur von dqe_tableau. %
% (siehe abschnitt 6.1 des kapitels 6) %
% %
% eingabe : eine positive quantorenfreie formel phi und elem. %
% ausgabe : phi', wobei phi' aus phi entsteht, indem ueberall %
% elem = 0 durch false ersetzt wird und %
% not(elem = 0) durch true ersetzt wird und %
% durch simplify vereinfacht wird. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_specneq(phi,elem);
begin scalar erg;
erg := dqe_simplify subst(t,list('neq,elem,0),
subst(nil,list('equal,elem,0),phi));
return erg;
end;
%%%%%%%%%%%%% dqe_specequal %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_specequal ist eine hilfsprozedur von dqe_tableau. %
% (siehe abschnitt 6.1 des kapitels 6) %
% %
% eingabe : eine positive quantorenfreie formel phi und elem. %
% ausgabe : phi', wobei phi' aus phi entsteht, indem ueberall %
% elem = 0 durch true ersetzt wird und %
% not(elem = 0) durch false ersetzt wird und mit hilfe%
% simplify vereinfacht wird. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_specequal(phi,elem);
begin scalar erg;
erg := dqe_simplify subst(t,list('equal,elem,0),
subst(nil,list('neq,elem,0),phi));
return erg;
end;
%%%%%%%%%%%%%%% dqe_tableau %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_tableau berechnet die tableau-methode fuer elem in der po-%
% tiven quantorenfreien formel phi. diese methode wurde in %
% abschnitt 6.1 des kapitels 6 dargestellt. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_tableau(phi,elem);
begin scalar erg;
erg := dqe_simplify(list('or,
list('and,list('equal,elem,0),dqe_specequal(phi,elem)),
list('and,list('neq,elem,0),dqe_specneq(phi,elem)) ));
if erg = list('or,list('equal,elem,0),list('neq,elem,0))
then erg := t;
return erg;
end;
%%%%%%%%%%% dqe_ltableau %%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_ltableau berechnet mehrere tableau-schritte. sie wurde in %
% abschnitt 6.1 spezifiziert. sie verwendet die obige prozedur %
% dqe_tableau. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_ltableau(phi,varliste);
begin scalar erg,elem;
erg := phi;
while varliste do
<< elem := car varliste;
varliste := cdr varliste;
erg := dqe_tableau(erg,elem)>>;
return erg;
end;
%%%%%%%%%%%%%%% dqe_dknfsimplify %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_dknfsimplify vereinfacht eine positive quantorenfreie formel, %
% die in disjunktiver bzw. konjunktiver normal form ist . %
% dqe_dknfsimplify verwendet die hilfsprozedur dqe_permutationfkt. %
% (siehe abschnitt 6.2 des kapitels 6) %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_dknfsimplify(phi);
begin scalar erg,hilf,hilff,liste,weiter,symb;
erg := nil;
if (phi = t) or (not phi)
or dqe_isatomarp(phi)
then erg := phi
else
<< symb := car phi;
phi := cdr phi;
while phi do
<< hilf := car phi ; phi := cdr phi;
if (hilf = t) or (not hilf)
or dqe_isatomarp(hilf)
then erg := dqe_modcons(hilf,erg)
else
<< liste := list(cadr hilf);
hilff := cddr hilf;
while hilff do
<< liste := dqe_consm(car hilff,liste);
hilff := cdr hilff >>;
if length(liste) = 1
then erg := dqe_modcons(car liste,erg)
else
<<hilf := cons(car hilf,reverse liste);
if not erg then erg := list(hilf)
else
if not(hilf member erg)
then
<< liste := erg; weiter := t;
while liste and weiter do
<< if dqe_listequal(hilf,car liste)
then weiter := nil
else liste := cdr liste >>;
if weiter
then erg := dqe_modcons(hilf,erg) >>
>> >> >>;
if length(erg) = 1
then erg := car erg
else
if cdr erg
then erg:= cons(symb,erg) >>;
return erg;
end;
%%%%%%%%%%%%%%% dqe_permutationfkt %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_permutationfkt ist eine hilfsprozedur fuer dqe_dknfsimplify.%
% sie berechnet alle permutation einer liste. %
% (siehe abschnitt 6.2 des kapitels 6) %
% %
% eingabe: eine liste phi von der form list(a_1,a_2,...,a_n), %
% wobei a_i paarweise verschieden sind und sie nur %
% atomare formeln oder true oder false seien duerfen. %
% %
% ausgabe: ergliste ist eine liste,die aus der menge der permu- %
% tation von der liste phi, falls phi mehr als ein ele- %
% enthaelt. %
% sonst ist ergliste leer. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_permutationfkt(phi);
begin scalar ergliste,liste,hilf,hilfliste,erghilf;
ergliste :=nil;
if not(phi) or (length(phi) = 1)
then ergliste := nil
else
if length(phi) = 2
then ergliste := list(phi,reverse phi)
else
<<liste := phi;
while liste do
<< hilf := car liste;
liste := cdr liste;
hilfliste := dqe_sanselem(phi,hilf);
hilfliste := dqe_permutationfkt(hilfliste);
while hilfliste do
<< erghilf := cons(hilf,car hilfliste);
ergliste := cons(erghilf,ergliste);
hilfliste := cdr hilfliste >> >>;
ergliste := reverse ergliste >>;
return ergliste;
end;
%%%%%%%%%%%%%%% dqe_sanselem %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% dqe_sanselem ist eine hilfsprozedur fuer dqe_permutationfkt . %
% (siehe abschnitt 6.2 des kapitels 6) %
% %
% eingabe: eine liste phi von der form list(a_1,a_2,...,a_n), %
% und eine element a. %
% %
% ausgabe: ergliste ist die liste phi ohne das element a. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
symbolic procedure dqe_sanselem(phi,elem);
begin scalar hilf,erg;
erg := nil;
while phi do
<< hilf := car phi;
phi := cdr phi;
if not(elem = hilf)
then erg := cons(hilf,erg) >>;
return reverse erg;
end;
% part 7
symbolic procedure dqe_pform f;
if listp f and car f eq '!*sq then prepsq cadr f else f$
endmodule; % [dcfsfkacem]
end; % of file