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.