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