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 L^AT_EX by H^EV^EA.

This document was cut into pieces by H^AC^HA.