A decision procedure for Direct Predicate Calculus. Study and implementation in the system Coq.
Résumé
The paper of J. Ketonen and R. Weyhrauch [6] defines a decidable fragment of first-order predicate logic - Direct Predicate Calculus - as the subset which is provable in Gentzen sequent calculus without the contraction rule, and gives an effective decision procedure for it. This report is a detailed study of this procedure. We extend the decidability to non-prenex formulas. We prove that the intuitionnistic fragment is still decidable, with a refinement of the same procedure. An intuitionnistic version has been implemented in the system Coq [2] using a translation into natural deduction.
L'article de J. Ketonen et R. Weyhrauch [6] définit un fragment décidable du calcul des prédicats du premier ordre - le Calcul des Prédicats Direct - comme le sous-ensemble prouvable dans le calcul des séquents de Gentzen sans utiliser la règle de contraction, et en donne une procédure de décision effective. Ce rapport présente une étude détaillée de cette procédure. Nous étendons la décidabilité au cas des formules non nécessairement prénexes. Nous montrons que le fragment intuitionniste est également décidable, par un raffinement de la même procédure. Une version intuitionniste de cette algorithme a été implémentée dans le système Coq [2].
Origine : Fichiers produits par l'(les) auteur(s)
Loading...