First - Order reasoning in the calculus of inductive constructions

Abstract

In this paper we present a contraction - free sequent calculus including inductive definitions for the first - order intuitionistic logic. We show that it is a natural extension to Dyckhoff's LJT calculus and we prove the contraction- and cut - elimination properties, thus extending Dyckhoff's result, in order to validate its use as a basis for proof - search procedures. Finally we describe the proof - search strategy used in our implementation as a tactic in the Coq proof assistant [2]. © Springer - Verlag 2004.