DFC-algorithms for Suszko logic and one-to-one Gentzen type formalizations

Studia Logica 43 (4):395 - 404 (1984)


We use here the notions and results from algebraic theory of programs in order to give a new proof of the decidability theorem for Suszko logic SCI (Theorem 3).We generalize the method used in the proof of that theorem in order to prove a more general fact that any prepositional logic which admits a cut-free Gentzen type formalization is decidable (Theorem 6).

Download options


    Upload a copy of this work     Papers currently archived: 72,805

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

29 (#399,324)

6 months
1 (#386,499)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Anita Wasilewska
State University of New York, Stony Brook

References found in this work

A Uniform Proof Procedure for SCI Tautologies.Aileen Michaels - 1974 - Studia Logica 33 (3):299 - 310.
A Sequence Formalization for SCI.Anita Wasilewska - 1976 - Studia Logica 35 (3):213 - 217.
On the Gentzen Type Formalizations.Anita Wasilewska - 1980 - Mathematical Logic Quarterly 26 (28-30):439-444.

Add more references

Citations of this work

Add more citations

Similar books and articles

Programs and Logics.Anita Wasilewska - 1985 - Studia Logica 44 (2):125 - 137.
Resolution Calculus for the First Order Linear Logic.Grigori Mints - 1993 - Journal of Logic, Language and Information 2 (1):59-83.
A Note on the Proof Theory the ╬╗II-Calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Gentzen-Type Systems, Resolution and Tableaux.Arnon Avron - 1993 - Journal of Automated Reasoning 10:265-281.