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 */