Programación lógica: Transformación B: -AC: -A a B, C: -A

Espero haber llegado al lugar correcto ... es (probablemente) una pregunta de programación lógica bastante sencilla.

Si tengo dos cláusulas de la forma: B:-A C:-A puedo transformarlas en: B,C:-A

( Editar: dónde B,Ces una conjunción. Estoy haciendo una evaluación de abajo hacia arriba y me es útil representar múltiples cláusulas con el mismo cuerpo usando una cláusula con una conjunción de los respectivos encabezados. Esto parece trivial, pero me pregunto si hay un nombre para tal transformación; sin embargo, sé que la cláusula resultante ya no es una cláusula Horn ) .

¿Alguien sabe si esta transformación tiene un nombre, y si es así, alguien puede proporcionar un puntero (preferiblemente en línea) a algún lugar que lo describa?

Muchas gracias (de un n00b).

$(A \supset B) \wedge (A \supset C)$$A \supset (B \wedge C)$$(B \supset A) \wedge (C \supset A)$$(B \vee C) \supset A$$A \supset B$$\supset$$\wedge$$\vee$

Lo que está tratando de hacer está relacionado con la transformación de binarización , que se trata en "Sobre el análisis de complejidad de los análisis estáticos" de McAllester. Puede haber un mejor nombre para la transformación, pero si es así, no se sabía los autores del artículo " Un solucionador sucinta de ALFP " ( Un lternating L al este F ixed p fórmulas OINT son una generalización de cláusulas de Horn para bottom programas lógicos como el suyo): en el Ejemplo 1 en la página 4, discuten una transformación similar y simplemente la llaman "explotar la posibilidad de compartir condiciones previas".

$mb:A\to B, mc:A\to C$$\langle mb, mc \rangle : A\to B\times C$