1:- module(folcnf,
    2		  [fol_cnf/2,factoring/2,elim_variant/2,
    3			cls_union/3,variant_memberchk/2,
    4			cnf_normal/2, cnf_variant_normal/2,
    5			ltr_check/4, cls_sort/2, tautology/1,
    6			unord_tautology/1, flip_polarity/2
    7		  ]).    8
    9:- use_module(pac(meta)).   10
   11:- current_op(P, T, (->)), member(T,[xfy, yfx, xfx]), op(P, T, '<-').   12:- current_op(P, T, (->)), member(T,[xfy, yfx, xfx]), op(P, T, '<--').   13:- current_op(P, T, (->)), member(T,[xfy, yfx, xfx]), op(P, T, '<-->').   14:- current_op(P, T, (->)), member(T,[xfy, yfx, xfx]), op(P, T, '<->').   15:- op(200, fy, ~).   16:- op(400, yfx, &).   17
   18% ?- fol_cnf(all(x, p== f(x))== (p==all(x, f(x))),  X),
   19%	numbervars(X), maplist(writeln, X).
   20
   21		/**********************************************
   22		*     (p==all(x, f(x))) == all(x, p==f(x))    *
   23		*	is not a theorem.						  *
   24		**********************************************/
   25
   26% ?- fol_cnf(-((p==all(x, f(x))) == all(x, p==f(x))), R), cnf_show(R).
   27% ?- fol_cnf((-p)*(p==all(x, f(x))), R), cnf_show(R).
   28% ?- fol_cnf(a, X).
   29% ?- fol_cnf(all(x, p==f(x))==(p==all(x, f(x))), R), cnf_show(R).
   30% ?- fol_cnf(- (all(x, p==f(x))==(p==all(x, f(x)))), R), cnf_show(R).
   31% ?- fol_cnf(a*a*b*a*b, R).
   32% ?- fol_cnf(a, R).
   33
   34%
   35fol_cnf(F, CNF):-
   36		do((	fol_skolemized_nnf,
   37%				factoring,
   38				cnf_normal,
   39				rm_tautology,
   40%				rm_unit,
   41				cnf_normal,
   42				cnf_variant_normal),
   43		   F, CNF).
   44%
   45q_assoc(X, Assoc, Y):- member(U-V, Assoc), X==U, !, Y = V.
   46%
   47q_subst(Assoc, A, A0):-
   48	(	q_assoc(A, Assoc, A0) ->  true
   49	;	var(A) -> A0 = A
   50	;	mapargs(q_subst(Assoc), A, A0)
   51	).
   52%
   53flip_polarity(-P, P):-!.
   54flip_polarity(P, -P).
   55
   56% ?- cls_sort([[],[]], R).
   57% ?- rm_unit([[a(X)],[-a(f(X))]], R).
   58% ?- rm_unit([[a(X)],[-a(X)]], R).
   59% ?- rm_unit([[a(X)],[-a(Y)]], R).
   60% ?- rm_unit([[a(X)],[-a(f(Y))]], R).
   61rm_unit(CNF, [[U]|CNF0]):-select([U], CNF, CNF1), !,
   62	flip_polarity(U, U0),
   63	rm_unit(U0, CNF1, CNF2),
   64	rm_unit(CNF2, CNF0).
   65rm_unit(CNF, CNF).
   66%
   67rm_unit(_, [], []):-!.
   68rm_unit(U, [C|CNF], [C0|CNF0]):-
   69	select(V, C, C0),
   70	variant(U, V),
   71	!,
   72	rm_unit(U, CNF, CNF0).
   73rm_unit(U, [C|CNF], [C|CNF0]):-rm_unit(U, CNF, CNF0).
   74
   75% ?- fol_skolemized_nnf(true, G).
   76% ?- fol_skolemized_nnf(-true, G).
   77% ?- fol_skolemized_nnf(-false, G).
   78% ?- fol_skolemized_nnf(a;b, G).
   79% ?- fol_skolemized_nnf(all(x, b(x)*c(x)), G).
   80% ?- fol_skolemized_nnf(some(x, b(x);c(x)), G).
   81% ?- fol_skolemized_nnf(all(y, some(x, b(x);c(y))), G).
   82% ?- fol_skolemized_nnf(all(y, some(x, b(x);c(x,y))), G).
   83% ?- fol_skolemized_nnf(- (all(y, f(y)==p) == (p==all(x, f(x)))), G), maplist(writeln, G).
   84
   85fol_skolemized_nnf(F, G):- intern(F, H),
   86	neg_normal(H, N),
   87	rename_bounded_vars(N, [], J),
   88	elim_quatifiers(J, K, [], Eqs, []),
   89	maplist(call, Eqs),
   90	nnf_cnf(K, G).
   91
   92% ?-  rename_bounded_vars(a, [], X).
   93% ?-  rename_bounded_vars(A, [], X).
   94% ?-  rename_bounded_vars(some(y, all(x, p(x);q(y))), [], X).
   95% ?-  neg_normal(-some(y, all(x, p(x);q(y))), U),
   96%	rename_bounded_vars(U, [], X).
   97% ?-  neg_normal(-some(x, all(x, p(x))*q(x)), U),
   98%	rename_bounded_vars(U, [], X).
   99
  100rename_bounded_vars(X, _, _):- var(X), !, throw(unboud_input).
  101rename_bounded_vars(some(X, B), Assoc, some(X0, B0)):-!,
  102	rename_bounded_vars(B, [X-X0|Assoc], B0).
  103rename_bounded_vars(some(X, D, B), Assoc, some(X0, D0, B0)):-!,
  104	rename_bounded_vars((B,D), [X-X0|Assoc], (B0, D0)).	% comma for pairing.
  105rename_bounded_vars(all(X, B), Assoc, all(X0, B0)):-!,
  106	rename_bounded_vars(B, [X-X0|Assoc], B0).
  107rename_bounded_vars(all(X, D, B), Assoc, all(X0, D0, B0)):-!,
  108	rename_bounded_vars((B,D), [X-X0|Assoc], (B0,D0)). % comma for pairing.
  109rename_bounded_vars(A*B, Assoc, A0*B0):-!,
  110	rename_bounded_vars(A, Assoc, A0),
  111	rename_bounded_vars(B, Assoc, B0).
  112rename_bounded_vars(A;B, Assoc, A0; B0):-!,
  113	rename_bounded_vars(A, Assoc, A0),
  114	rename_bounded_vars(B, Assoc, B0).
  115rename_bounded_vars(-X, Assoc, -X0):-!,
  116	rename_bounded_vars(X, Assoc, X0).
  117rename_bounded_vars(X, Assoc, Y):- X=..[F|Xs],
  118	maplist(q_subst(Assoc), Xs, Ys),
  119	Y =..[F|Ys].
  120
  121% ?- neg_normal(- (a* b), X).
  122% ?- neg_normal(a * -B, X).
  123% ?- neg_normal(-(-(X)), Y).
  124% ?- neg_normal(- - -a, Y).
  125% ?- neg_normal(X, Y).
  126% ?- neg_normal(some(X,m(X)* -(all(A, n(A), -(Y)))), U).
  127% ?- neg_normal(-(x==y), U).
  128% ?- neg_normal(x==y, U), neg_normal(-U, V).
  129% ?- write_canonical(-a * -b).
  130
  131neg_normal(X, _)		:- var(X), !, throw(unboud_input).
  132neg_normal(-X, -X)		:- var(X), !, throw(unboud_formula).
  133neg_normal(-(-X), Z)	:-!, neg_normal(X, Z).
  134neg_normal(-(X;Y), Z)	:-!, neg_normal(-X* -Y, Z).
  135neg_normal(-(X*Y), Z)	:-!, neg_normal(-X; -Y, Z).
  136neg_normal(-(X->Y), Z)	:-!, neg_normal(-(-X; Y), Z).
  137neg_normal(-(<-(X,Y)), Z):-!, neg_normal(-(Y->X), Z).
  138neg_normal(-(X==Y), Z)	:-!, neg_normal(- ((X->Y)*(Y->X)), Z).
  139neg_normal(-all(X,Y), Z):-!, neg_normal(some(X, -Y), Z).
  140neg_normal(-all(X, D, Y), Z):-!, neg_normal(some(X, D, -Y), Z).
  141neg_normal(-some(X,Y), Z):-!, neg_normal(all(X, -Y), Z).
  142neg_normal(-some(X, D, Y), Z):-!, neg_normal(all(X, D, -Y), Z).
  143neg_normal(X;Y, X0;Y0)	:-!, neg_normal(X, X0), neg_normal(Y, Y0).
  144neg_normal(X*Y, X0*Y0)	:-!, neg_normal(X, X0), neg_normal(Y, Y0).
  145neg_normal(X==Y, Z)		:-!, neg_normal((X->Y)*(Y->X), Z).
  146neg_normal(X->Y, Z)		:-!, neg_normal(-X;Y, Z).
  147neg_normal(<-(X,Y), Z)	:-!, neg_normal(Y->X, Z).
  148neg_normal(all(X, Y), all(X, Z)):-!, neg_normal(Y, Z).
  149neg_normal(all(X, D, Y), all(X, D, Z)):-!, neg_normal(Y, Z).
  150neg_normal(some(X, Y), some(X, Z)):-!, neg_normal(Y, Z).
  151neg_normal(some(X, D, Y), some(X, D, Z)):-!, neg_normal(Y, Z).
  152neg_normal(-true, ff)	:-!.
  153neg_normal(-tt, ff)		:-!.
  154neg_normal(-false, tt)	:-!.
  155neg_normal(-ff, tt)		:-!.
  156neg_normal(true, tt)	:-!.
  157neg_normal(false, ff)	:-!.
  158neg_normal(X, X).
  159
  160% ?- elim_quatifiers(a, X, [], E, []).
  161% ?- elim_quatifiers(some(x, p(x)), X, [], E, []).
  162% ?- elim_quatifiers((some(x, -p(x))* some(y, p(y))), X, [], E, []).
  163% ?- elim_quatifiers((some(x, p(x))*some(x, p(x))), X, [], E, []).
  164
  165elim_quatifiers(some(X, B), B0, Vs, [X=SKterm|Eqs], Eqs0):-!,
  166	gensym(sk, F),
  167	SKterm=..[F|Vs],
  168	elim_quatifiers(B, B0, Vs, Eqs, Eqs0).
  169elim_quatifiers(all(X, B), B0, Vs, Eqs, Eqs0):-!,
  170	elim_quatifiers(B, B0, [X|Vs], Eqs, Eqs0).
  171elim_quatifiers(A*B, A0*B0, Vs, Eqs, Eqs0):-!,
  172	elim_quatifiers(A, A0, Vs, Eqs, Eqs1),
  173	elim_quatifiers(B, B0, Vs, Eqs1, Eqs0).
  174elim_quatifiers(A;B, A0;B0, Vs, Eqs, Eqs0):-!,
  175	elim_quatifiers(A, A0, Vs, Eqs, Eqs1),
  176	elim_quatifiers(B, B0, Vs, Eqs1, Eqs0).
  177elim_quatifiers(X, X, _, Eqs, Eqs).
  178
  179% ?- extern(all(X, some(Y, love(X,Y); love(Y,X))), A), print(A).
  180canonical_op(C, D, Cs, E):-
  181	member(M, Cs),
  182	memberchk(C, M),
  183	member(D, E),
  184	memberchk(D, M).
  185%
  186connectives([ [ ',', (*),  (&), and],
  187	      [;, + , '|', or],
  188	      [(\+), ~, not, -],
  189	      [(->), imply, =>],
  190	      [<-],
  191	      [iff, <->, == , =:= , <=>, <-->],
  192	      [every, all, forall],
  193	      [some, exists, ex] ]).
  194
  195% ?- write((a, b|c, d)).
  196internal_op([*, ;, -, ->, ==, all, some]).
  197
  198% ?- internal_op(and, X).
  199internal_op(C, D):- connectives(Cs),
  200	internal_op(E),
  201	canonical_op(C, D, Cs, E).
  202%
  203external_op([*, ;, -, ->, ==, all, some]).
  204
  205% ?- external_op((or), X).
  206external_op(C, D):- connectives(Cs),
  207	external_op(E),
  208	canonical_op(C, D, Cs, E).
  209
  210% ?- intern(some(x, all(y, a(x, y))), R).
  211% ?- intern(some(x, all(y, a(x, (y,z)))), R).
  212% ?- intern(some(x, all(y, all(x, (y,z)))), R).
  213% ?- intern(some(x, p(x)->q(x)), R).
  214% ?- intern(x=y, R).
  215% ?- intern((a,b), R).
  216% ?- intern(and(a,b), R).
  217% ?- intern(or(a,b), R).
  218% ?- intern(a == b, R).
  219% ?- intern(-(a == b), R).
  220% ?- intern(some(x, d(x), p(x)), R).
  221% ?- intern(-some(x, d(x), p(x)), R).
  222% ?- nnf_skolem(-(a == b), R).
  223% ?- intern(or(a,b), R), extern(R, E).
  224% ?- extern(imply(a,imply(b,c)), R), extern(R, E).
  225
  226intern(X, X)	:- var(X), !.
  227intern(X->Y, Z)	:-!, intern(-(X);Y, Z).
  228intern(X==Y, Z)	:-!, intern((X*Y);(-X)*(-Y), Z).
  229intern(X, Y)	:- X =..[F|As], internal_op(F, G), !,
  230		maplist(intern, As, Bs),
  231		Y =..[G|Bs].
  232intern(X, X).
  233
  234%
  235extern(X, X):- var(X), !.
  236extern(X, Y):- X =..[F|As], external_op(F, G), !,
  237		maplist(extern, As, Bs),
  238		Y =..[G|Bs].
  239extern(X, X).
  240
  241%
  242cnf_normal(X, Y):-maplist(cls_sort, X, X0), cnf_sort(X0, Y).
  243%
  244cnf_variant_normal(X, Y):-maplist(cls_sort, X, X0),
  245	elim_variant(X0, X1),
  246	cnf_sort(X1, Y).
  247
  248% ?- fol_cnf(a*b, R).
  249% ?- fol_cnf(all(X, (a(X)*b(X))), R).
  250% ?- fol_cnf(all(X, (-a(X); b(X);a(X))), R).
  251% ?- fol_cnf(all(X, (g,(-a(X); b(X);a(X)))), R).
  252% ?- fol_cnf(a; some(x, b(x)), X).
  253% ?- fol_cnf(all(X, (-a(X); b(X);a(X))), R).
  254nnf_cnf(A*B,C):-!,
  255	nnf_cnf(A,A0),
  256	nnf_cnf(B,B0),
  257	cnf_union(A0,B0,C0),
  258	cnf_sort(C0, C).
  259nnf_cnf(A;B, C):-!,
  260	nnf_cnf(A,A0),
  261	nnf_cnf(B,B0),
  262	cnf_distribute(A0,B0,C).
  263nnf_cnf(tt, []):-!.
  264nnf_cnf(ff, [[]]):-!.
  265nnf_cnf(A, [[A]]).

 fol_ltr_compare(-C, +X, +Y) is det

Compare literals X and Y, and C is unified with <, =, > as the standard compare/3. ex. a<b, a < -a, -a < b, -a < -b.

  272fol_ltr_compare(C, -X, -Y):-!, compare(C, X, Y).
  273fol_ltr_compare(C, X, -Y):-!, compare(C0, X, Y),
  274		(	C0 == (=) ->  C =(<)
  275		;	C = C0
  276		).
  277fol_ltr_compare(C, -X, Y):-!, compare(C0, X, Y),
  278		(	C0 == (=) -> C = (>)
  279		;	C = C0
  280		).
  281fol_ltr_compare(C, X, Y):- compare(C, X, Y).
  282
  283% ?- cls_sort([-a, b, a, -b, a], R).
  284% ?- cls_sort([], R).
  285% ?- cls_sort([-a(X), a(X), -b, a], L).
  286cls_sort(X, Y):- predsort(fol_ltr_compare, X, Y).
  287
  288% ?- cls_compare(C, [a],[b]).
  289% ?- cls_compare(C, [a],[]).
  290% ?- cls_compare(C, [],[]).
  291cls_compare(C, X, Y):- length(X, L), length(Y, M),
  292	(	L = M -> cls_compare_same_length(C, X, Y)
  293	;	L < M -> C = (<)
  294	;	C = (>)
  295	).
  296%
  297cls_compare_same_length(=, [], []):-!.
  298cls_compare_same_length(C, [X|Xs], [Y|Ys]):- fol_ltr_compare(D, X, Y),
  299	(  D = (=) -> cls_compare_same_length(C, Xs, Ys)
  300	;  C = D
  301	).
  302
  303% ?- ltr_check(a(1), S, X, R).
  304% ?- ltr_check(-a(1), S, X, R).
  305ltr_check(-X, S, X, P/N):-!, S = (-), functor(X, P, N).
  306ltr_check(X, S, X, P/N):- S = (+), functor(X, P, N).
  307
  308% ?- cnf_sort([[a(X), -b(A), c(A)],[-a(X), b(Y)]], X).
  309cnf_sort(X, Y):- predsort(cls_compare, X, Y).
  310
  311% ?- unord_tautology([a(X), -a(X), c, -d]).
  312% ?- unord_tautology([a(X), -a(Y), c, -d]).  % false
  313unord_tautology([-A|As]):- member(B, As), A == B, !.
  314unord_tautology([A|As]):- member(B, As), (-A) == B, !.
  315unord_tautology([_|As]):- unord_tautology(As).
  316%
  317tautology(X):- ord_tautology(X).
  318
  319% ?- ord_tautology([a, b, -b, d]).
  320ord_tautology([P, -Q|_]):- P == Q, !.
  321ord_tautology([_|R]):- ord_tautology(R).
  322
  323%
  324tautology_law(X, Y):- rm_tautology(X,Y).
  325
  326% ?- rm_tautology([[a, -a, b], [c]], R).
  327rm_tautology([], []):-!.
  328rm_tautology([C|Cs], Ds):- tautology(C), !,
  329	rm_tautology(Cs, Ds).
  330rm_tautology([C|Cs], [C|Ds]):- rm_tautology(Cs, Ds).
  331
  332%
  333unify(X, Y):- unify_with_occurs_check(X, Y).
  334
  335% ?- cnf_show([[a],[b]]).
  336cnf_show(X, Y):- writeln(X), !, cnf_show(Y).
  337%
  338cnf_show(Cs):- forall(member(X, Cs), (numbervars(X), writeln(X))),
  339	writeln('---------\n').
  340
  341%
  342set_when_gt(I, J, S):-
  343	(	I =< J -> true
  344	;	nb_setarg(1, S, 1)
  345	).
  346%
  347apply_options([], X, X).
  348apply_options([P|Ps], X, Y):- call(P, X, Z),
  349	apply_options(Ps, Z, Y).
  350
  351%
  352variant_memberchk(X, [Y|_]) :- variant(X, Y), !.
  353variant_memberchk(X, [_|Ys]):- variant_memberchk(X, Ys).
  354
  355% ?- cls_union([a(X), a(Y)],[a(Y), b(Z)], U).
  356cls_union([], X, X):-!.
  357cls_union(X, [], X):-!.
  358cls_union([X|U], [Y|V], W):- fol_ltr_compare(C, X, Y),
  359	(	C = (=)	->
  360		cls_union(U, V, W0),
  361		W = [X|W0]
  362	;	C = (<)	->
  363		cls_union(U, [Y|V], W0),
  364		W = [X|W0]
  365	;	cls_union([X|U], V, W0),
  366		W = [Y|W0]
  367	).
  368
  369% ?- cls_meet([a(Y), a(X)], [a(Y), b(Z)], M).
  370cls_meet([], _, []):-!.
  371cls_meet(_, [], []):-!.
  372cls_meet([X|U], [Y|V], W):- fol_ltr_compare(C, X, Y),
  373	(	C = (=)	->	cls_meet(U, V, W0), W =[X|W0]
  374	;	C = (<)	->	cls_meet(U, [Y|V], W)
  375	;	cls_meet([X|U], V, W)
  376	).
  377
  378% ?- subtract([a(X), a(Y)], [a(Z)], R).
  379% ?- cls_subtract([a(X), a(Y)], [a(Z)], R).
  380% ?- cls_subtract([a(X), a(Y)], [a(Y)], R).
  381cls_subtract([], _, []):-!.
  382cls_subtract(X, [], X):-!.
  383cls_subtract([X|U], [Y|V], W):- fol_ltr_compare(C, X, Y),
  384	(	C = (=)	-> cls_subtract(U, V, W)
  385	;	C = (<)	->
  386		cls_subtract(U, [Y|V], W0),
  387		W = [X|W0]
  388	;	cls_subtract([X|U], V, W)
  389	).
  390
  391% ?- ltr_insert(b(Z),[a(Y), b(Z)], U).
  392% ?- ltr_insert(c(Z),[a(Y), b(Z)], U).
  393ltr_insert(L, [], [L]):-!.
  394ltr_insert(L, [X|Xs], Y):-  fol_ltr_compare(C, L, X),
  395	(	C=(=) -> Y = [X|Xs]
  396	;	C=(<) -> Y = [L|[X|Xs]]
  397	;	ltr_insert(L, Xs, Us),
  398		Y = [X|Us]
  399	).
  400
  401% ?- cnf_distribute([[[a]]], [[[b]],[[c]]], R).
  402cnf_distribute([], _, []).
  403cnf_distribute([A|R], X, P):- maplist(cls_union(A), X, Q),
  404	cnf_distribute(R, X, R0),
  405	cnf_union(Q, R0, P).
  406
  407% ?- cnf_union([[a(X), a(Y)]],[[a(Y), b(Z)]], U), cnf_union(U, U, W).
  408cnf_union([], X, X):-!.
  409cnf_union(X, [], X):-!.
  410cnf_union([X|U], [Y|V], W):- cls_compare(C, X, Y),
  411	(	C = (=)	->
  412		cnf_union(U, V, W0),
  413		W = [X|W0]
  414	;	C = (<)	->
  415		cnf_union(U, [Y|V], W0),
  416		W = [X|W0]
  417	;	cnf_union([X|U], V, W0),
  418		W = [Y|W0]
  419	).
  420
  421% ?- cnf_meet([[a(X)],[b(Y)]], [[b(Y)],[c(Y)]], U).
  422% ?- cnf_meet([[a(X)],[b(Y)]], [[b(Z)],[c(Y)]], U).   % U = [].
  423cnf_meet([], _, []):-!.
  424cnf_meet(_, [], []):-!.
  425cnf_meet([X|U], [Y|V], W):-cls_compare(C, X, Y),
  426	(	C = (=)	->	cnf_meet(U, V, W0), W = [X|W0]
  427	;	C = (<)	->	cnf_meet(U, [Y|V], W)
  428	;	cnf_meet([X|U], V, W)
  429	).
  430
  431% ?- cnf_subtract([[a(X), a(Y)]], [[a(Z)]], R).
  432% ?- cnf_subtract([[a(X)],[a(Y)]], [[a(Y)]], R).
  433cnf_subtract([], _, []):-!.
  434cnf_subtract(X, [], X):-!.
  435cnf_subtract([X|U], [Y|V], W):-cls_compare(C, X, Y),
  436	(	C = (=)	-> cnf_subtract(U, V, W)
  437	;	C = (<)	->
  438		cnf_subtract(U, [Y|V], W0),
  439		W = [X|W0]
  440	;	cnf_subtract([X|U], V, W)
  441	).
  442
  443% ?- cls_insert([a,b], [[b,c]], X).
  444% ?- cls_insert([b(X),c(Y)], [[a(Z),b(U)]], X).
  445cls_insert(X, [], [X]):-!.
  446cls_insert(X, [Y|Ys], Z):- cls_compare(C, X, Y),
  447	(	C = (=) -> Z = [Y|Ys]
  448	;	C = (<) -> Z = [X|[Y|Ys]]
  449	;	cls_insert(X, Ys, Z0),
  450		Z = [Y|Z0]
  451	).

?- elim_variant([[a(X), a(Y)], [a(A), a(B)]], R). ?- elim_variant([[a, a], [a, a]], U).

  455elim_variant([], []):-!.
  456elim_variant([C|Cs], [C|Ds]):- elim_variant(C, Cs, Es),
  457	elim_variant(Es, Ds).
  458%
  459elim_variant(_, [], []):-!.
  460elim_variant(C, [C0|Cs], Ds):- variant(C, C0), !,
  461	elim_variant(C, Cs, Ds).
  462elim_variant(C, [C0|Cs], [C0|Ds]):- elim_variant(C, Cs, Ds).
  463
  464% ?- fol_cnf(a, R), factoring(R, F).
  465% ?- fol_cnf((a,b), R), factoring(R, F).
  466% ?- fol_cnf((a(A);a(B);a(C)), R), factoring(R, F), length(F, N),
  467%	maplist(writeln, F).
  468%
  469factoring(CNF, F):-
  470	maplist(cls_factoring, CNF, Factors),
  471	maplist(unify_list_of_factors, Factors, List),
  472	append(List, F).
  473
  474% ?- unify_list_of_factors([[[a(A), a(1)], [b(B), b(2)]], [[a(A), a(2)], [b(B), b(1)]]], R).
  475
  476unify_list_of_factors([], []).
  477unify_list_of_factors([B|Bs], F):-
  478	copy_term(B, B0),
  479	(	unify_factors(B0, F0) ->
  480		F = [F0|R]
  481	;	F = R
  482	),
  483	unify_list_of_factors(Bs, R).
  484
  485% ?- unify_factors([[a(A), a(1)], [b(B), b(2)]], X).
  486unify_factors([], []).
  487unify_factors([[A]|R], [A|R0]):-!, unify_factors(R, R0).
  488unify_factors([[A|As]|R], [A|R0]):-!, unify_factor(As, A),
  489	unify_factors(R, R0).
  490%
  491unify_factor([], _).
  492unify_factor([B|Bs], A):- unify_with_occurs_check(A, B),
  493		unify_factor(Bs, A).
  494
  495% ?- list_partition([a, b], X).
  496% ?- time((N = 10, numlist(1, N, Ns), list_partition(Ns, X), length(X, L))).
  497
  498list_partition([],[[]]).
  499list_partition([X|Y], Z):- list_partition(Y, Ps),
  500	add_one(Ps, X, Z).
  501%
  502add_one([], _, []).
  503add_one([P|Ps], X, [[[X]|P]|U]):-
  504	add_one_to_each_block(P, X, V),
  505	add_one(Ps, X, W),
  506	append(V, W, U).
  507%
  508add_one_to_each_block([], _, []).
  509add_one_to_each_block([B|Bs], X, [[[X|B]|Bs]|U]):-
  510	add_one_to_each_block(Bs, X, V),
  511	map_cons(V, B, U).
  512
  513% ?- map_cons([[a],[b]], c, X).
  514map_cons(X, Y, Z):- map_cons(X, Y, Z, []).
  515%
  516map_cons([], _, U, U).
  517map_cons([P|Ps], X, [[X|P]|U], V):- map_cons(Ps, X, U, V).
  518
  519% ?- cls_factoring([], X).
  520% ?- cls_factoring([a,b], X).
  521% ?- cls_factoring([a(1),a(2), b, c], X).
  522% ?- cls_factoring([a(1),a(2), -a(3), -a(4), c], X), maplist(writeln, X).
  523
  524cls_factoring(X, Y):-  cls_sort(X, Z),
  525	ord_ltr_group(Z, U),
  526	maplist(list_partition, U, V),
  527	product_with_append(V, Y).
  528
  529% ?- ord_ltr_group([], X).
  530% ?- ord_ltr_group([a], X).
  531% ?- ord_ltr_group([a,b,c], X).
  532% ?- ord_ltr_group([a(1),a(2), -a(1), -a(2), c], X).
  533%@ X = [[a(1), a(2)], [-a(1), -a(2)], [c]].
  534ord_ltr_group([], [[]]).
  535ord_ltr_group([X|Y], Z):- ord_ltr_group(Y, U),
  536	ord_ltr_group(U, X, Z).
  537%
  538ord_ltr_group([[]|R], X, [[X]|R]):-!.
  539ord_ltr_group([[A|U]|R], X, [[X,A|U]|R]):-ltr_same_group(X, A), !.
  540ord_ltr_group(R, X, [[X]|R]).
  541
  542% ?- ltr_same_group(a, -a).
  543ltr_same_group(X, Y):- ltr_check(X, S, _, B),
  544					   ltr_check(Y, S, _, B).
  545
  546% ?- product_with_append([], X).
  547% ?- product_with_append([[[a]]], X).
  548% ?- product_with_append([[[a]], [[b]]], X).
  549% ?- product_with_append([[[a,b], [c,d]], [[b],[d]]], X).
  550
  551product_with_append([], [[]]).
  552product_with_append([X|Y], Z):- product_with_append(Y, U),
  553	product_with_append(X, U, Z, []).
  554%
  555product_with_append([], _, Z, Z).
  556product_with_append([X|Xs], Y, Z, U):-
  557	product_with_append_base(Y, X, Z, V),
  558	product_with_append(Xs, Y, V, U).
  559%
  560product_with_append_base([], _, Z, Z).
  561product_with_append_base([Y|Ys], X, [V|Z], U):-
  562	append(X, Y, V),
  563	product_with_append_base(Ys, X, Z, U)