This paper studies decidable fragments of the predicate calculus. We will focus on the structure of Direct Predicate Calculus as defined by Ketonen and Weyrauch [1984] in the light of recent work by Girard [1987,1988] 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.
A decision procedure revisited: Notes on direct logic, linear logic and its implementation
BELLIN, Gianluigi;
1992-01-01
Abstract
This paper studies decidable fragments of the predicate calculus. We will focus on the structure of Direct Predicate Calculus as defined by Ketonen and Weyrauch [1984] in the light of recent work by Girard [1987,1988] 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.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
1-s2.0-030439759290069R-main.pdf
accesso aperto
Tipologia:
Documento in Post-print
Licenza:
Dominio pubblico
Dimensione
2.75 MB
Formato
Adobe PDF
|
2.75 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
