A Decision Procedure Revisited: Notes on Direct Logic, Linear Logic and its Implementation

G Bellin and J Ketonen

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.

LFCS report ECS-LFCS-91-167

Previous | Index | Next