## 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