Calcul des séquents

5 Calcul des séquents

Inconvénient de la résolution : perte de structure des formules pour la démonstration.

Le calcul des séquents propositionnel peut être étendu au calcul des prédicats en ajoutant des règles pour traiter les quantificateurs.

S;p(t), G ¾® D

S;"x.p(x) Î G ¾® D

"_G

S+c;G ¾® p(c), D

S;G ¾® "x.p(x), D

"_D

S+c;p(c), G ¾® D

S;$x.p(x), G ¾® D

$_G

S;G ¾® p(t), D

S;G ¾® $x.p(x)Î D

$_D

dans les règles "_G et $_D, t désigne un terme quelconque sur la signature S ;
dans les règles "_D et $_G, c désigne une nouvelle constante qui est ajoutée à la signature pour la suite du calcul.

Pratiquement, dans le cas d'une preuve faite en chaînage arrière, on ne peut pas « deviner » le terme t au moment de l'utilisation de la règle "_G ou $_D : on laisse une variable qui sera remplacée par le terme lui-même le moment voulu (en respectant la contrainte sur les constantes universelles).

Exemple : S={f₁, a₀}, |=^?(" x p(x)) ® " y p(f(y))

t = f(c)

S+c;p(t) ¾® p(f(c))

axiome

S+c;" x p(x) ¾® p(f(c))

"_G t est un S+c-terme

S;" x p(x) ¾® " y p(f(y))

"_D c est une nouvelle constante

S; ¾® (" x p(x)) ® " y p(f(y))

® _D

Exercice :

Essayer d'appliquer "_G avant "_D dans cette démonstration.
|=^?(" x p(f(x))) ® " y p(y)