Tableaux, connexions et couplages
Jean Goubault-Larrecq
Une utilisation plus directe du système LK de Gentzen est, comme
dans le cas propositionnel, la méthode des tableaux. Bien qu'elle
n'ait pas bénéficié d'autant de raffinements que la
résolution, elle s'appuie sur un formalisme plus propre, à savoir
LK sans la règle de coupure. De plus, comme les preuves sans
coupure sont déjà (presque) canoniques sans que l'on ait besoin de
raffiner la méthode, on peut espérer que l'espace de recherche des
preuves sera considérablement plus petit qu'avec la résolution.
Comme nous le verrons, ce n'est pas tout à fait vrai.
Nous présentons la méthode de base en section 1.
Nous la raffinons en la méthodes des tableaux à variables
libres en section 2, et nous décrivons en
section 3 la méthode très proche des
connexions, aussi connue sous le nom de méthode des couplages
(``matings'' en anglais). Nous comparons ces méthodes à certaines
variantes de la résolution en section 3.2, ce qui
montrera que ces méthodes ne sont pas si éloignées les unes des
autres.
This document was translated from LATEX by HEVEA.
This document was cut into pieces by
HACHA.