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\chapter[Die Datei {\tt tom\_merge\_clauses}]{Die Datei {\Huge \tt tom\_merge\_clauses}}
   17
   18\Predicate merge_clauses/3 (+ClauseList1, +ClauseList2, -MergedClauseList).
   19
   20The clauses of this predicate try to merge two lists of clauses.
   21The predicate basically performs a cross prduct on the elements of
   22the lists |ClauseList1| and |ClauseList2|.
   23
   24Assuming, we have two list \((x_1)_{i=1,\ldots,n}\) and \((y_j)_{j=1,\ldots,m}\),
   25the cross product is a list \((f(x_i,y_j))_{i = 1,\ldots,n \atop j = 1,
   26\ldots,m}\). The function \(f\) is analysing the structure of the terms \(x_i\)
   27and \(y_i\).
   28
   29The code for this is adapted from
   30
   31\begin{center}
   32Richard O'Keefe\\
   33The Craft of Prolog\\
   34MIT Press, Cambridge, Mass.\\
   351990, p.\ 243
   36\end{center}
   37
   38\PL*/
   39
   40merge_clauses([],_,[]).
   41merge_clauses([Clause | ClauseList1],ClauseList2,EntryList):-
   42	merge_clauses(ClauseList2,Clause,EntryList,Accumulator),
   43	merge_clauses(ClauseList1,ClauseList2,Accumulator).
   44
   45merge_clauses([],_) --> [].
   46merge_clauses([ Clause | ClauseList1 ],ClauseList2) -->
   47	{ merge_to_formula(Clause,ClauseList2,ResultingClause) },
   48	[ResultingClause],
   49	merge_clauses(ClauseList1,ClauseList2).
   50
   51/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   52
   53\Predicate merge_to_formula/3 (+Clause1, +Clause2, -MergedClause).
   54
   55If we have two terms or formulas, their structures are analysed within the
   56predicate |merge_to_formula/3|.
   57
   58We merge the two clauses according to the usual propositional
   59equivalences:
   60\begin{eqnarray*}
   61(\varphi_1 \to \psi_1) \vee (\varphi_2 \to \psi_2) & = & (\varphi_1 \wedge \varphi_2) \to (\psi_1 \vee \psi_2)\\
   62(\varphi_1 \to \psi_1) \vee \varphi_2 & = & \varphi_1 \to (\psi_1 \vee \psi_2)\\
   63\varphi_1 \vee (\varphi_2 \to \psi_2) & = & \varphi_2 \to (\varphi_1 \vee \psi_2)
   64\end{eqnarray*}
   65
   66\PL*/
   67
   68merge_to_formula(L1, L2, Clause):-
   69	( L1 = implies (Prem1, Conc1) ->
   70	    ( L2 = implies(Prem2, Conc2) ->
   71	         Clause = implies(and(Prem1,Prem2), or(Conc1,Conc2))
   72	    ; Clause = implies(Prem1, or(Conc1,L2))
   73	    )
   74	;   ( L2 = implies(Prem2, Conc2) ->
   75	        Clause = implies(Prem2, or(Conc2,L1))
   76	    ; Clause = or(L1, L2)
   77	    )
   78	).
   79/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   80\EndProlog */