A decision procedure for Direct Predicate Calculus. Study and implementation in the system Coq.

Abstract : 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.
Document type :
Reports
Complete list of metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101905
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:09:26 AM
Last modification on : Friday, May 17, 2019 - 1:39:21 AM

File

RR1996-25.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101905, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

2

Files downloads

6