J.-C. Filliātre. A decision procedure for Direct Predicate Calculus: study and implementation in the Coq system. Research Report 96-25, LIP - ENS Lyon, February 1995.

The paper of J. Ketonen and R. Weyhrauch A decidable fragment of Predicate Calculus 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 Coq system using a translation into natural deduction.

[ bib | .ps.Z ]

Back