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).


2 Answers 2


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.")

What you're trying to do is related to the binarization transformation, which is discussed in McAllester's "On the complexity analysis of static analyses." There may be a better name for the transformation, but if so, it wasn't known the authors of the paper "A succinct solver for ALFP" (Alternating Least Fixedpoint formulas are a generalization of Horn clauses for bottom-up logic programs such as yours) - in Example 1 on page 4 they discuss a similar transformation and just call it "exploiting the possibility of sharing of pre-conditions."

  • 1
    $\begingroup$ Man, I have got to stop shallow parsing whole fields of research, and getting my education from Wikipedia. Maybe then I can find out what the wheel is called before I reinvent it. (But first I need to finish my PhD o.O) $\endgroup$
    – badroit
    Dec 7, 2010 at 3:52
  • $\begingroup$ Sorry for my wrong answer. I shouldn't post late in the evening. $\endgroup$ Dec 7, 2010 at 9:28
  • $\begingroup$ I understand the feeling (applies to both comments!) $\endgroup$ Dec 7, 2010 at 19:13

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.