%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% $Id: merge.pl,v 1.5 1995/01/27 13:45:38 gerd Exp $
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 
%%% This file is part of ProCom.
%%% It is distributed under the GNU General Public License.
%%% See the file COPYING for details.
%%% 
%%% (c) Copyright 1995 Gerd Neugebauer
%%% 
%%% Net: gerd@imn.th-leipzig.de
%%% 
%%%****************************************************************************

/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

\Predicate merge_clauses/3 (+ClauseList1, +ClauseList2, -MergedClauseList).

The clauses of this predicate try to merge two lists of clauses.
The predicate basically performs a cross prduct on the elements of
the lists |ClauseList1| and |ClauseList2|.

Assumed we have two list \((x_1)_{i=1,\ldots,n}\) and \((y_j)_{j=1,\ldots,m}\),
the cross product is a list \((f(x_i,y_j))_{i = 1,ldots,n \atop j = 1,
\ldots,m}. The function \(f\) is analysing the structure of the terms \(x_i\)
and \(y_i\).

The code for this is adapted from Richard O'Keefe's ``The Craft of Prolog'',
MIT Press, Cambridge, Mass., 1990, p.\ 243.

\PL*/
merge_clauses([],_,[]).
merge_clauses([Clause | ClauseList1],ClauseList2,EntryList):-
	merge_clauses(ClauseList2,Clause,EntryList,Accumulator),
	merge_clauses(ClauseList1,ClauseList2,Accumulator).

merge_clauses([],_) --> [].
merge_clauses([ Clause | ClauseList1 ],ClauseList2) -->
	{ merge_to_formula(Clause,ClauseList2,ResultingClause) },
	[ResultingClause],
	merge_clauses(ClauseList1,ClauseList2).
/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

\Predicate merge_to_formula/3 (+Clause1, +Clause2, -MergedClause).

If we have two terms or formulas, their structures are analysed within the
predicate |merge_to_formula/3|.

We merge the two clauses according to the usual propositional
equivalences:
\begin{eqnarray*}
(\varphi_1 \to \psi_1) \vee (\varphi_2 \to \psi_2) & = & (\varphi_1 \wedge \varphi_2) \to (\psi_1 \vee \psi_2)\\
(\varphi_1 \to \psi_1) \vee \varphi_2 & = & \varphi_1 \to (\psi_1 \vee \psi_2)\\
\varphi_1 \vee (\varphi_2 \to \psi_2) & = & \varphi_2 \to (\varphi_1 \vee \psi_2)
\end{eqnarray*}

\PL*/
merge_to_formula(L1, L2, Clause):-
	( L1 =.. [implies, Prem1, Conc1] ->
	    ( L2 =.. [implies, Prem2, Conc2] ->
	         Clause =.. [implies, and(Prem1,Prem2), or(Conc1,Conc2)]
	    ; Clause =.. [implies, Prem1, or(Conc1,L2)]
	    )
	;   ( L2 =.. [implies, Prem2, Conc2] ->
	        Clause =.. [implies, Prem2, or(Conc2,L1)]
	    ; Clause =.. [or, L1, L2]
	    )
       ).
/*PL%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
\EndProlog */