A decision procedure for Direct Predicate Calculus. Study and implementation in the system Coq. - LARA - Libre accès aux rapports scientifiques et techniques Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1995

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].
Fichier principal
Vignette du fichier
RR1996-25.pdf (371.82 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02101905 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02101905 , version 1

Citer

Jean-Christophe Filliatre. A decision procedure for Direct Predicate Calculus. Study and implementation in the system Coq.. [Research Report] LIP RR-1996-25, Laboratoire de l'informatique du parallélisme. 1995, 2+32p. ⟨hal-02101905⟩
10 Consultations
113 Téléchargements

Partager

Gmail Facebook X LinkedIn More