reduce-historical/r38/packages/redlog/ofsfbnf.red

% ----------------------------------------------------------------------
% $Id: ofsfbnf.red,v 1.9 2003/06/11 08:46:55 dolzmann Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-2003 A. Dolzmann, A. Seidl, and T. Sturm
% ----------------------------------------------------------------------
% $Log: ofsfbnf.red,v $
% Revision 1.9  2003/06/11 08:46:55  dolzmann
% Implemented black boxes rl_qssimpl and rl_qssiadd.
%
% Revision 1.8  2003/06/04 06:10:22  dolzmann
% Added black box implementation ofsf_qssusuat.
%
% Revision 1.7  2003/06/03 16:10:39  dolzmann
% Added blackbox implementations for rl_qssubsumep, rl_qstrycons, and
% rl_qssubat.
%
% Revision 1.6  2003/05/27 08:19:19  dolzmann
% Changed wrong log messages.
%
% Revision 1.5  2003/05/27 08:17:42  dolzmann
% Added pseudo implementation of black box cl_qscsa.
%
% Revision 1.4  1999/03/23 07:41:37  dolzmann
% Changed copyright information.
%
% Revision 1.3  1999/03/21 13:38:04  dolzmann
% Removed procedure acfsf_bnfsimpl which was identical to cl_bnfsimpl.
%
% Revision 1.2  1996/10/07 12:03:22  sturm
% Added fluids for CVS and copyright information.
%
% Revision 1.1  1996/03/22 12:14:02  sturm
% Moved and split.
%
% ----------------------------------------------------------------------
lisp <<
   fluid '(ofsf_bnf_rcsid!* ofsf_bnf_copyright!*);
   ofsf_bnf_rcsid!* := "$Id: ofsfbnf.red,v 1.9 2003/06/11 08:46:55 dolzmann Exp $";
   ofsf_bnf_copyright!* :=
      "Copyright (c) 1995-2003 by A. Dolzmann, A. Seidl, and T. Sturm"
>>;

module ofsfbnf;
% Ordered field standard form boolean normal forms. Submodule of [ofsf].

procedure ofsf_dnf(f);
   % Ordered field standard form conjunctive normal form. [f] is a
   % formula. Returns a DNF of [f].
   if !*rlbnfsac then
      (cl_dnf f) where !*rlsiso=T
   else
      cl_dnf f;

procedure ofsf_cnf(f);
   % Ordered field standard form conjunctive normal form. [f] is a
   % formula. Returns a CNF of [f].
   if !*rlbnfsac then
      (cl_cnf f) where !*rlsiso=T
   else
      cl_cnf f;

procedure ofsf_subsumption(l1,l2,gor);
   % Ordered field standard form subsume. [l1] and [l2] are lists of
   % atomic formulas. Returns one of [imp], [rep], [nil].
   if gor eq 'or then (
      if ofsf_subsumep!-and(l1,l2) then
 	 'keep2
      else if ofsf_subsumep!-and(l2,l1) then
	 'keep1
   ) else  % [gor eq 'and]
      if ofsf_subsumep!-or(l1,l2) then
	 'keep1
      else if ofsf_subsumep!-or(l2,l1) then
	 'keep2;

procedure ofsf_subsumep!-and(l1,l2);
   % Ordered field standard form subsume [and] case. [l1] and [l2] are
   % lists of atomic formulas.
   begin scalar a;
      while l2 do <<
	 a := car l2;
	 l2 := cdr l2;
	 if cl_simpl(a,l1,-1) neq 'true then a := l2 := nil
      >>;
      return a
   end;

procedure ofsf_subsumep!-or(l1,l2);
   % Ordered field standard form subsume [or] case. [l1] and [l2] are
   % lists of atomic formulas.
   begin scalar a;
      while l1 do <<
	 a := car l1;
	 l1 := cdr l1;
	 if cl_simpl(rl_smkn('or,l2),{a},-1) neq 'true then a := l1 := nil
      >>;
      return a
   end;

procedure ofsf_sacatlp(a,l);
   % Ordered field standard form subsume and cut atomic formula list
   % predicate. [a] is an atomic formula; [l] is a list of atomic
   % formulas. [T] is returned if a subsumption or cut beween [a] and
   % an element of [l] is possible.
   not ((ofsf_arg2l a neq ofsf_arg2l w) and ordp(ofsf_arg2l a,ofsf_arg2l w))
      where w=car l;

procedure ofsf_sacat(a1,a2,gor);
   % Ordered field standard form subsume and cut atomic formula. [a1]
   % and [a2] are atomic formulas; [gor] is one of [or], [and].
   % Returns [nil], ['keep], ['keep2], ['keep1], ['drop], or an atomic
   % formula. If [nil] is returned then neither a cut nor a
   % subsumption can be applied, if [keep] is returned then the atomic
   % formuas are identical, in the case of [keep1] or [keep2] the
   % respective atomic formula must be kept but the other can be
   % dropped. If an atomic formula $a$ is returned then it is the
   % result of the cut beween [a1] and [a2], if ['drop] is returned, a
   % cut with result ['true] or ['false] can be performed.
   begin scalar w;
      if ofsf_arg2l a1 neq ofsf_arg2l a2 then return nil;
      w := ofsf_sacrel(ofsf_op a1, ofsf_op a2,gor);
      if w memq '(drop keep keep1 keep2) then return w;
      return ofsf_0mk2(w,ofsf_arg2l a1)
   end;

procedure ofsf_sacrel(r1,r2,gor);
   % Ordered field standard form subsume and cut relation. [r1] and
   % [r2] are relations; [gor] is one of [or], [and]. Returns ['keep],
   % ['keep2], ['keep1], ['drop], or a relation. [r1] and [r2] are
   % considered as relations of atomic formulas $[r1](t,0)$ and
   % $[r2](t,0)$. If [keep] is returned then the atomic formulas are
   % identical, in the case of [keep1] or [keep2] the respective
   % atomic formula must be kept but the other can be dropped, if a
   % relation $\rho$ is returned a cut with result $t\rho 0$ can be
   % performed, where $t$ is the left hand side of [a1] and [a2], if
   % ['drop] is returned, a cut with result ['true] or ['false] can be
   % performed.
   if gor eq 'or then
      ofsf_sacrel!-or(r1,r2)
   else
      ofsf_sacrel!-and(r1,r2);

procedure ofsf_sacrel!-or(r1,r2);
   % Ordered field standard form subsume and cut relation or. [r1] and
   % [r2] are relations. ['keep], ['keep2], ['keep1], ['drop], or a
   % relation is returned. [r1] and [r2] are considered as relations
   % of atomic formulas $[r1](t,0)$ and $[r2](t,0)$. If [keep] is
   % returned then the atomic formulas are identical, in the case of
   % [keep1] or [keep2] the respective atomic formula must be kept but
   % the other can be dropped, if a relation $\rho$ is returned a cut
   % with result $t\rho 0$ can be performed, where $t$ is the left
   % hand side of [a1] and [a2], if ['drop] is returned a cut with
   % result ['true] can be performed.
   begin scalar w;
      w:= '( (lessp . ( (lessp . keep) (leq . keep1) (equal . leq)
                        (neq . keep1) (geq . drop) (greaterp . neq)))
	     (leq   . ( (lessp . keep2) (leq . keep) (equal . keep2)
		        (neq . drop) (geq . drop) (greaterp . drop)))
	     (equal . ( (lessp . leq) (leq . keep1) (equal . keep)
		        (neq . drop) (geq . keep1) (greaterp . geq)))
	     (neq   . ( (lessp . keep2) (leq . drop) (equal . drop)
		        (neq . keep) (geq . drop) (greaterp . keep2)))
	     (geq   . ( (lessp . drop) (leq . drop) (equal . keep2)
		        (neq . drop) (geq . keep) (greaterp . keep2)))
	     (greaterp . ( (lessp . neq)  (leq . drop)  (equal . geq)
	             	(neq . keep1) (geq . keep1) (greaterp . keep))));
      return cdr atsoc(r1,cdr atsoc(r2,w));
   end;

procedure ofsf_sacrel!-and(r1,r2);
   % Ordered field standard form subsume and cut relation and. [r1] and
   % [r2] are relations. ['keep], ['keep2], ['keep1], ['drop], or a
   % relation is returned. [r1] and [r2] are considered as relations
   % of atomic formulas $[r1](t,0)$ and $[r2](t,0)$. If [keep] is
   % returned then the atomic formulas are identical, in the case of
   % [keep1] or [keep2] the respective atomic formula must be kept but
   % the other can be dropped, if a relation $\rho$ is returned a cut
   % with result $t\rho 0$ can be performed, where $t$ is the left
   % hand side of [a1] and [a2], if ['drop] is returned a cut with
   % result ['false] can be performed.
   begin scalar w;
      w:= '( (lessp . ( (lessp . keep) (leq . keep2) (equal . drop)
                        (neq . keep2) (geq . drop) (greaterp . drop)))
	     (leq   . ( (lessp . keep1) (leq . keep) (equal . keep1)
		        (neq . lessp) (geq . equal) (greaterp . drop)))
	     (equal . ( (lessp . drop) (leq . keep2) (equal . keep)
		        (neq . drop) (geq . keep2) (greaterp . drop)))
	     (neq   . ( (lessp . keep1) (leq . lessp) (equal . drop)
		        (neq . keep) (geq . greaterp) (greaterp . keep1)))
	     (geq   . ( (lessp . drop) (leq . equal) (equal . keep1)
		        (neq . greaterp) (geq . keep) (greaterp . keep1)))
	     (greaterp . ( (lessp . drop)  (leq . drop)  (equal . drop)
	             	(neq . keep2) (geq . keep2) (greaterp . keep))));
      return cdr atsoc(r1,cdr atsoc(r2,w))
   end;

% ----------------------------------------------------------------------
% Simplification of Boolean normal forms in the style of W. V. Quine.
% ----------------------------------------------------------------------

procedure ofsf_qssubat(pl,a);
   begin scalar w,r;
      w := ofsf_qssubatfind(pl,a);
      if not w then
	 return a;
      r := ofsf_qssubatrel(ofsf_op w,ofsf_op a);      
      return if rl_tvalp r then
	 r
      else
	 ofsf_0mk2(r,ofsf_arg2l a)
   end;

procedure ofsf_qssubatfind(pl,a);
   begin scalar r,la;
      la := ofsf_arg2l a;
      while pl do <<
	 if ofsf_arg2l car pl = la then <<
	    r := car pl;
	    pl := nil
	 >> else
	    pl := cdr pl
      >>;
      return r
   end;

% TODO: Reuse tables of ofsfsism
procedure ofsf_qssubatrel(r1,r2);
   begin scalar w;
      % Printen mit: for each x in w do << for each y in cdr x do <<
      % prin2 cdr y; prin2 "  " >>; prin2t ""; >>;
      w:= '( (lessp . ( (lessp . true) (leq . true) (equal . false)
                        (neq . true) (geq . false) (greaterp . false)))
	     (leq   . ( (lessp . neq) (leq . true) (equal . geq)
		        (neq . neq) (geq . geq) (greaterp . false)))
	     (equal . ( (lessp . false) (leq . true) (equal . true)
		        (neq . false) (geq . true) (greaterp . false)))
	     (neq   . ( (lessp . leq) (leq . leq) (equal . false)
		        (neq . true) (geq . geq) (greaterp . geq)))
	     (geq   . ( (lessp . false) (leq . leq) (equal . leq)
		        (neq . neq) (geq . true) (greaterp . neq)))
	     (greaterp . ( (lessp . false)  (leq . false)  (equal . false)
	             	(neq . true) (geq . true) (greaterp . true))));
      return cdr atsoc(r2,cdr atsoc(r1,w))
   end;
   
procedure ofsf_qstrycons(a,c1,c2,op);
   % quine simplification try consensus. [a] is an atomic formula,
   % [c1] and [c2] are clauses, op is one of ['and], ['or]. Returns
   % [T], [nil] or [break]. [c1] contains [a].
   begin scalar r,cc1,cc2,w;
      w := ofsf_qstrycons!-find(a,c2);
      if null w then
	 return nil;
      r := ofsf_qstrycons!-or(ofsf_op a,ofsf_op w);
      if null r or r eq 'false then
	 return nil;
      cc1 := delete(a,c1);  % Copy... % TODO: delq or delete?
      cc2 := delete(w,c2);  % Copy... % TODO: delq or delete?
      w := append(cc1,cc2);  % TODO: nconc
      if r neq 'true then
      	 w := ofsf_0mk2(r,ofsf_arg2l a) . w;	    
      w := cl_qssimplc(w,nil,op);  % TODO: CNF
      if w eq 'false then
	 return nil;
      if w eq 'true then
	 return 'break;
%%       prin2t "Konsens von";
%%       mathprint rl_prepfof rl_smkn('and,c1);
%%       prin2t "Mit";
%%       mathprint rl_prepfof rl_smkn('and,c2);
%%       prin2t "Ueber";
%%       mathprint rl_prepfof a;
%%       prin2t "Ergibt";
%%       mathprint rl_prepfof rl_smkn('and,w);
      return w
   end;

procedure ofsf_qstrycons!-or(r1,r2);
   begin scalar w;      
      w := ofsf_qsflip ofsf_smeqtable(ofsf_qsflip r1,ofsf_qsflip r2);
      return if w eq r1 or w eq r2 then nil else w
   end;	 

procedure ofsf_qsflip(r);
   if rl_tvalp r then
      cl_flip r
   else
      ofsf_lnegrel r;
	 
% (TODO) REMARK: Letters occurs only once.

procedure ofsf_qstrycons!-find(a,c2);
   begin scalar r,la;
      la := ofsf_arg2l a;
      while c2 do <<
	 if ofsf_arg2l car c2 = la then <<
	    r := car c2;
	    c2 := nil
	 >> else
	    c2 := cdr c2;
      >>;
      return r
   end;

procedure ofsf_qssusuat(a1,a2,op);
   ofsf_arg2l a1 = ofsf_arg2l a2 and ofsf_qssusutab(ofsf_op a1,ofsf_op a2);

% TODO: Abbrechen bei offensichtlichem widerspruch
procedure ofsf_qssusutab(r1,r2);
   begin scalar w;
      % Printen mit: for each x in w do << for each y in cdr x do <<
      % prin2 cdr y; prin2 "  " >>; prin2t ""; >>;
      w:= '( (lessp . ( (lessp . T) (leq . T) (equal . nil)
                        (neq . T) (geq . nil) (greaterp . nil)))
	     (leq   . ( (lessp . nil) (leq . T) (equal . nil)
		        (neq . nil) (geq . nil) (greaterp . nil)))
	     (equal . ( (lessp . nil) (leq . T) (equal . T)
		        (neq . nil) (geq . T) (greaterp . nil)))
	     (neq   . ( (lessp . nil) (leq . nil) (equal . nil)
		        (neq . T) (geq . nil) (greaterp . nil)))
	     (geq   . ( (lessp . nil) (leq . nil) (equal . nil)
		        (neq . nil) (geq . T) (greaterp . nil)))
	     (greaterp . ( (lessp . nil)  (leq . nil)  (equal . nil)
	             	(neq . T) (geq . T) (greaterp . T))));
      return cdr atsoc(r2,cdr atsoc(r1,w))
   end;

procedure ofsf_qssiadd(a,c,theo);
   begin scalar w;
      w := ofsf_qssifind(a,c);
      if null w then
	 return a . c;
      c := delq(w,c);
      w := ofsf_qssibin(a,w);
      return if rl_tvalp w then
	 w
      else
	 w . c
   end;

procedure ofsf_qssibin(a1,a2);
   begin scalar w;
      w := ofsf_qssirel(ofsf_op a1,ofsf_op a2);
      if rl_tvalp w then
	 return w;
      return ofsf_0mk2(w,ofsf_arg2l a1);
   end;

procedure ofsf_qssifind(a,c);
   begin scalar r,la;
      la := ofsf_arg2l a;
      while c do <<
	 if ofsf_arg2l car c = la then <<
	    r := car c;
	    c := nil
	 >> else
	    c := cdr c
      >>;
      return r
   end;

procedure ofsf_qssirel(r1,r2);
   begin scalar w;
      % Printen mit: for each x in w do << for each y in cdr x do <<
      % prin2 cdr y; prin2 "  " >>; prin2t ""; >>;
      w:= '( (lessp . ( (lessp . lessp) (leq . lessp) (equal . false)
                        (neq . lessp) (geq . false) (greaterp . false)))
	     (leq   . ( (lessp . lessp) (leq . leq) (equal . equal)
		        (neq . lessp) (geq . equal) (greaterp . false)))
	     (equal . ( (lessp . false) (leq . equal) (equal . equal)
		        (neq . false) (geq . equal) (greaterp . false)))
	     (neq   . ( (lessp . lessp) (leq . lessp) (equal . false)
		        (neq . neq) (geq . greaterp) (greaterp . greaterp)))
	     (geq   . ( (lessp . false) (leq . equal) (equal . equal)
		        (neq . greaterp) (geq . geq) (greaterp . greaterp)))
	     (greaterp . ( (lessp . false)  (leq . false)  (equal . false)
		        (neq . greaterp) (geq . greaterp) (greaterp . greaterp)
		   )));
      return cdr atsoc(r2,cdr atsoc(r1,w))
   end;

endmodule;  % [ofsfbnf]

end;  % of file