1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%% $Id: merge.pl,v 1.5 1995/01/27 13:45:38 gerd Exp $
    3%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    4%%% 
    5%%% This file is part of ProCom.
    6%%% It is distributed under the GNU General Public License.
    7%%% See the file COPYING for details.
    8%%% 
    9%%% (c) Copyright 1995 Gerd Neugebauer
   10%%% 
   11%%% Net: gerd@imn.th-leipzig.de
   12%%% 
   13%%%****************************************************************************
   14
   15/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   16
   17\Predicate merge_clauses/3 (+ClauseList1, +ClauseList2, -MergedClauseList).
   18
   19The clauses of this predicate try to merge two lists of clauses.
   20The predicate basically performs a cross prduct on the elements of
   21the lists |ClauseList1| and |ClauseList2|.
   22
   23Assumed we have two list \((x_1)_{i=1,\ldots,n}\) and \((y_j)_{j=1,\ldots,m}\),
   24the cross product is a list \((f(x_i,y_j))_{i = 1,ldots,n \atop j = 1,
   25\ldots,m}. The function \(f\) is analysing the structure of the terms \(x_i\)
   26and \(y_i\).
   27
   28The code for this is adapted from Richard O'Keefe's ``The Craft of Prolog'',
   29MIT Press, Cambridge, Mass., 1990, p.\ 243.
   30
   31\PL*/
   32merge_clauses([],_,[]).
   33merge_clauses([Clause | ClauseList1],ClauseList2,EntryList):-
   34	merge_clauses(ClauseList2,Clause,EntryList,Accumulator),
   35	merge_clauses(ClauseList1,ClauseList2,Accumulator).
   36
   37merge_clauses([],_) --> [].
   38merge_clauses([ Clause | ClauseList1 ],ClauseList2) -->
   39	{ merge_to_formula(Clause,ClauseList2,ResultingClause) },
   40	[ResultingClause],
   41	merge_clauses(ClauseList1,ClauseList2).
   42/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   43
   44\Predicate merge_to_formula/3 (+Clause1, +Clause2, -MergedClause).
   45
   46If we have two terms or formulas, their structures are analysed within the
   47predicate |merge_to_formula/3|.
   48
   49We merge the two clauses according to the usual propositional
   50equivalences:
   51\begin{eqnarray*}
   52(\varphi_1 \to \psi_1) \vee (\varphi_2 \to \psi_2) & = & (\varphi_1 \wedge \varphi_2) \to (\psi_1 \vee \psi_2)\\
   53(\varphi_1 \to \psi_1) \vee \varphi_2 & = & \varphi_1 \to (\psi_1 \vee \psi_2)\\
   54\varphi_1 \vee (\varphi_2 \to \psi_2) & = & \varphi_2 \to (\varphi_1 \vee \psi_2)
   55\end{eqnarray*}
   56
   57\PL*/
   58merge_to_formula(L1, L2, Clause):-
   59	( L1 =.. [implies, Prem1, Conc1] ->
   60	    ( L2 =.. [implies, Prem2, Conc2] ->
   61	         Clause =.. [implies, and(Prem1,Prem2), or(Conc1,Conc2)]
   62	    ; Clause =.. [implies, Prem1, or(Conc1,L2)]
   63	    )
   64	;   ( L2 =.. [implies, Prem2, Conc2] ->
   65	        Clause =.. [implies, Prem2, or(Conc2,L1)]
   66	    ; Clause =.. [or, L1, L2]
   67	    )
   68       ).
   69/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   70\EndProlog */