-
19SN and CR for Free-Style LKtq: Linear Decorations and Simulation of NormalizationJournal of Symbolic Logic 67 (1). 2002.The present report is a, somewhat lengthy, addendum to [4], where the elimination of cuts from derivations in sequent calculus for classical logic was studied 'from the point of view of linear logic'. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between multiplicative and additive versions of the binary connectives. The main novelty here is the observation that this type-distinction is not essential: we can allow classical sequent derivatio…Read more
-
30From abstraction and indiscernibility to classification and typesKagaku Tetsugaku 53 (2): 65-93. 2021.
-
17SN and CR for free-style LKtq: linear decorations and simulation of normalizationJournal of Symbolic Logic 67 (1): 162-196. 2002.
-
34LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implicationIn Jean-Yves Girard, Yves Lafont & Laurent Regnier (eds.), Advances in linear logic, Cambridge University Press. pp. 222--211. 1995.
-
9Revised version of a conference given under title "From Natural Deduction to the nature of reasoning", at the colloquium Natural Deduction organized by Luiz Carlos Pereira and dedicated to the work of Dag Prawitz, Rio de Janeiro, Brazil, July 2001.
-
6A New Deconstructive Logic: Linear LogicJournal of Symbolic Logic 62 (3): 755-807. 1997.The main concern of this paper is the design of a noetherian and confluent normalization for $\mathbf{LK}^2$. The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's $\mathbf{LC}$ and Parigot's $\lambda\mu, \mathbf{FD}$, delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' to classical logic; it is painless: since we reduce strong normalization and confluenc…Read more
-
25SN and {CR} for free-style {${bf LK}sp {tq}$}: linear decorations and simulation of normalizationJournal of Symbolic Logic 67 (1): 162-196. 2002.The present report is a, somewhat lengthy, addendum to "A new deconstructive logic: linear logic," where the elimination of cuts from derivations in sequent calculus for classical logic was studied ‘from the point of view of linear logic’. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between multiplicative and additive versions of the binary connectives.The main novelty here is the observation that this type-distinction is not essential: we…Read more
-
41Completeness of MLL Proof-Nets w.r.t. Weak DistributivityJournal of Symbolic Logic 72 (1). 2007.We examine 'weak-distributivity' as a rewriting rule $??$ defined on multiplicative proof-structures (so, in particular, on multiplicative proof-nets: MLL). This rewriting does not preserve the type of proof-nets, but does nevertheless preserve their correctness. The specific contribution of this paper, is to give a direct proof of completeness for $??$: starting from a set of simple generators (proof-nets which are a n-ary ⊗ of &-ized axioms), any mono-conclusion MLL proof-net can be reached by…Read more
-
84A new deconstructive logic: Linear logicJournal of Symbolic Logic 62 (3): 755-807. 1997.The main concern of this paper is the design of a noetherian and confluent normalization for LK 2. The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD, delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' to classical logic ; it is painless: since we reduce strong normalization and confluence to the same properties for linear logi…Read more
-
38On the linear decoration of intuitionistic derivationsArchive for Mathematical Logic 33 (6): 387-412. 1995.We define an optimal proof-by-proof embedding of intuitionistic sequent calculus into linear logic and analyse the (purely logical) linearity information thus obtained
Areas of Specialization
Science, Logic, and Mathematics |
Metaphysics and Epistemology |
Areas of Interest
Science, Logic, and Mathematics |
Metaphysics and Epistemology |