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