Logique basique LPO, Méthode de résolution de Robinson (avec principe de réfutation)
Bonjour à toutes et à tous,
J'ouvre cette discussion afin de vous demander quels résultats vous trouvez au sujet de cette question:
{A ∨ B ∨ ¬D ; A ∧ B => C} |= (A => C ∧ D)
En utilisant, bien évidemment, la méthode de résolution de Robinson (avec principe de réfutation, c'est à dire qu'on ajoute la négation de la conséquence sémantique dans l'ensemble de formules afin d'essayer de trouver une clause vide, ce qui prouverait la déduction originale).
Merci d'avance pour vos réponses !
-----