# Logic Programming: Transforming B:-A C:-A to B,C:-A

I hope I've come to the right place... it's (probably) a fairly straightforward Logic Programming question.

If I have two clauses of the form: B:-A C:-A I can transform these into: B,C:-A

(Edit: where B,C is a conjunction. I'm doing bottom-up evaluation and it's useful to me to represent multiple clauses with the same body using one clause with a conjunction of the respective heads. This seems trivial, but I'm wondering if there's a name for such a transformation—however, I know that the resulting clause is no longer a Horn clause.)

Does anyone know if this transformation has a name, and if so, can anyone provide a pointer (preferably online) to somewhere that describes it.

Many thanks (from a n00b).

So, this is an instance of the fact that $(A \supset B) \wedge (A \supset C)$ is equivalent to $A \supset (B \wedge C)$. A different type isomorphism, namely that $(B \supset A) \wedge (C \supset A)$ is equivalent to $(B \vee C) \supset A$, looks more like what you wrote down, but that's because in logic programming notation we write B :- A when we mean $A \supset B$. (Note: $\supset$ is "implies," $\wedge$ is "and," and $\vee$ is "or.")
In the context of CCC, your transformation is interpreted as “$mb:A\to B, mc:A\to C$ is transformed to $\langle mb, mc \rangle : A\to B\times C$”, i.e. the product of morphisms.