Quelques raffinements de la résolution propositionnelle
Jean Goubault-Larrecq
Le but de cette note est de montrer comment obtenir certains des
raffinements usuels de la résolution --- hyperrésolution,
résolution sémantique, raffinements ordonnés --- par des
techniques à la Gentzen de réécriture de preuves dans LK0.
Ces techniques s'étendront au premier ordre naturellement, par la
technique standard de relèvement (lifting en anglais).
This document was translated from LATEX by HEVEA.
This document was cut into pieces by
HACHA.