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/*%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   16
   17\Predicate mymerge/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
   23Assuming, 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*/
   32
   33mymerge([],_,[]).
   34mymerge([Clause | ClauseList1],ClauseList2,EntryList):-
   35	mymerge(ClauseList2,Clause,EntryList,Accumulator),
   36	mymerge(ClauseList1,ClauseList2,Accumulator).
   37
   38mymerge([],_) --> [].
   39mymerge([ Clause | ClauseList1 ],ClauseList2) -->
   40	{ merge_to_formula(Clause,ClauseList2,ResultingClause) },
   41	[ResultingClause],
   42	mymerge(ClauseList1,ClauseList2).
   43
   44/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   45
   46\Predicate merge_to_formula/3 (+Clause1, +Clause2, -MergedClause).
   47
   48If we have two terms or formulas, their structures are analysed within the
   49predicate |merge_to_formula/3|.
   50
   51We merge the two clauses according to the usual propositional
   52equivalences:
   53\begin{eqnarray*}
   54(\varphi_1 \to \psi_1) \vee (\varphi_2 \to \psi_2) & = & (\varphi_1 \wedge \varphi_2) \to (\psi_1 \vee \psi_2)\\
   55(\varphi_1 \to \psi_1) \vee \varphi_2 & = & \varphi_1 \to (\psi_1 \vee \psi_2)\\
   56\varphi_1 \vee (\varphi_2 \to \psi_2) & = & \varphi_2 \to (\varphi_1 \vee \psi_2)
   57\end{eqnarray*}
   58
   59\PL*/
   60
   61merge_to_formula(L1, L2, Clause):-
   62	( L1 =.. [implies, Prem1, Conc1] ->
   63	    ( L2 =.. [implies, Prem2, Conc2] ->
   64	         Clause =.. [implies, and(Prem1,Prem2), or(Conc1,Conc2)]
   65	    ; Clause =.. [implies, Prem1, or(Conc1,L2)]
   66	    )
   67	;   ( L2 =.. [implies, Prem2, Conc2] ->
   68	        Clause =.. [implies, Prem2, or(Conc2,L1)]
   69	    ; Clause =.. [or, L1, L2]
   70	    )
   71       ).
   72/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   73\EndProlog */