Calcul en logique du premier ordre

Un calcul logique, au sens large, est une méthode de résolution appliquée au
traitement d’une structure propositionnelle. Les propositions constituant
cette structure peuvent aussi bien être des expressions d’une langue naturelle
(comme le français) que des expressions d’un langage formalisé (comme
l’arithmétique), liées entre elles par une dépendance de nature fonctionnelle.
Cet ouvrage constitue une introduction à deux outils de calcul en logique du
premier ordre, soit le calcul en arbres de consistance et le calcul en
déduction naturelle. La première partie, centrée sur la notion de structure
propositionnelle, expose les concepts, les objets et les méthodes propres à la
logique propositionnelle. Dans la deuxième partie, la logique propositionnelle
est étendue à la logique prédicative au moyen de la quantification et de
concepts caractéristiques d’un langage du premier ordre. Les deux outils de
calcul sont ensuite enrichis de manière à pouvoir traiter des fonctions
propositionnelles, soit des prédicats du premier ordre. De nombreux exemples
et exercices, accompagnés de leurs solutions, aideront l’étudiant à progresser
vers des calculs toujours plus complexes et à raffiner ses méthodes de calcul
logique.