Queridos todos
Limitémonos a las teorías lógicas que consisten sólo en fórmulas $P_1 \supset \quad ... \quad P_n \supset Q$ , es decir, cláusulas de cuerno proposicional expresadas con implicación. Supongamos sólo un subconjunto de la lógica mínima, no (->R), sólo (->L).
Mi punto de partida es el siguiente cálculo muy primitivo:
$${P \in \Gamma \over \Gamma \Rightarrow P}{(init)} \qquad {(P \supset A) \in \Gamma \qquad \Gamma \Rightarrow P \qquad \Gamma, A \Rightarrow Q \over \Gamma \Rightarrow Q}{({\supset}L)}$$
Cuando enfocamos el (->L) que la cabeza de A coincide con el objetivo Q, entonces obtenemos el encadenamiento hacia atrás.
$${(P_1 \supset \quad ... \quad P_n \supset Q) \in \Gamma \qquad \Gamma \Rightarrow P_1 \quad ... \quad \Gamma \Rightarrow P_n \over \Gamma \Rightarrow Q}{({\supset}L \quad Back)}$$
Ahora estoy experimentando con otra variante de (->L). En lugar de requerir que la cabeza machte el objetivo, requiero que los átomos del cuerpo ya estén dados:
$${(P_1 \supset \quad ... \quad P_n \supset Q) \in \Gamma \qquad P_1 \in \Gamma \qquad ... \qquad P_n \in \Gamma \qquad \Gamma, Q \Rightarrow R \over \Gamma \Rightarrow R}{({\supset}L \quad Forward)}$$
El encadenamiento hacia adelante se ha caracterizado por derivar nuevos hechos a partir de hechos dados. Surgen un par de preguntas:
* Is the forward chaining variant of the primitive calculus still complete?
* Is forward chaining also a from of focusing?
* Are there better ways to formulate forward chaining than with (->L Forward)?Saludos cordiales
P.D: La pregunta está inspirada en el cálculo replanteado en ¿Cómo se establece la conversión de una prueba sin cortes en una prueba uniforme?
P.S.S.: Aquí hay un ejemplo de una prueba de encadenamiento hacia atrás:
-------------- (init)
p, p -> q => p
-------------- (->L Back)
p, p -> q => q Y aquí hay un ejemplo de prueba de encadenamiento hacia adelante:
----------------- (init)
p, p -> q, q => q
----------------- (->L Forward)
p, p -> q => q
