Skip to main content

Bounded contraction in systems with linearity

Citations of this article
Mendeley users who have this article in their library.
Get full text


The aim of this work is to perform a proof-theoretical investigation of some propositional logics underlying either finite-valued Godel logic or finite-valued Lukasiewicz logic. We define cut-free hyper- sequent calculi for logics obtained by adding either the n-contraction law or the n-weak law of excluded middle to affine intuitionistic linear logic with the linearity axiom (A→B) V (B→A). We also develop cut-free calculi for the classical counterparts of these logics. Moreover we define a hypersequent calculus for L3∩L4 in which the cut-elimination theorem holds. This calculus allows to define an alternative axiomatization of L4 making no use of the Lukasiewicz axiom.




Ciabattoni, A. (1999). Bounded contraction in systems with linearity. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1617, pp. 113–128). Springer Verlag.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free