%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% $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 %%% %%%**************************************************************************** /*%^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ \chapter[Die Datei {\tt tom\_merge\_clauses}]{Die Datei {\Huge \tt tom\_merge\_clauses}} \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|. Assuming, 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 \begin{center} Richard O'Keefe\\ The Craft of Prolog\\ MIT Press, Cambridge, Mass.\\ 1990, p.\ 243 \end{center} \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 */