Résolution au premier ordre
Jean Goubault-Larrecq
Nous avons déjà présenté la résolution comme une méthode
de preuve automatique pour la logique propositionnelle classique.
Bien qu'elle n'était pas l'une des méthodes les plus efficaces
dans ce contexte, elle peut être optimisée de nombreuses
façons. De plus, elle est utile pour présenter les outils
fondamentaux dont nous avons besoin pour la recherche de preuve en
logique classique du premier ordre sans que l'on ait à s'occuper de
complications provenant de problèmes purement propositionnels.
This document was translated from LATEX by HEVEA.
This document was cut into pieces by
HACHA.