Abstract: This paper studies decidable fragments of predicate calculus. We will focus on the structure of Direct Predicate Calculus as defined in [KETONEN and WEYHRAUCH 1984] in the light of the recent work of Girard [GIRARD 1987, 1988 A and B] on Linear Logic. Several graph-theoretic results are used to prove correspondences between systems of Natural Deduction, Direct Predicate Logic, and Linear Logic. In addition, the implementation of a decision procedure for Direct Predicate Logic is sketched.
Previous | Index | Next