Author name cluster

Roberto Maieli

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

2 author rows

CSL Conference 2020 Conference Paper

Generalized Connectives for Multiplicative Linear Logic

Matteo Acclavio
Roberto Maieli

In this paper we investigate the notion of generalized connective for multiplicative linear logic. We introduce a notion of orthogonality for partitions of a finite set and we study the family of connectives which can be described by two orthogonal sets of partitions. We prove that there is a special class of connectives that can never be decomposed by means of the multiplicative conjunction ⊗ and disjunction ⅋, providing an infinite family of non-decomposable connectives, called Girard connectives. We show that each Girard connective can be naturally described by a type (a set of partitions equal to its double-orthogonal) and its orthogonal type. In addition, one of these two types is the union of the types associated to a family of MLL-formulas in disjunctive normal form, and these formulas only differ for the cyclic permutations of their atoms.

Details

LPAR Conference 2007 Conference Paper

Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic

Roberto Maieli

Abstract Proof nets are a parallel syntax for sequential proofs of linear logic, firstly introduced by Girard in 1987. Here we present and intrinsic (geometrical) characterization of proof nets, that is a correctness criterion (an algorithm) for checking those proof structures which correspond to proofs of the purely multiplicative and additive fragment of linear logic. This criterion is formulated in terms of simple graph rewriting rules and it extends an initial idea of a retraction correctness criterion for proof nets of the purely multiplicative fragment of linear logic presented by Danos in his Thesis in 1990.

Details

I&C Journal 2003 Journal Article

Non-commutative logic III: focusing proofs

Roberto Maieli
Paul Ruet

It is now well-established that the so-called focalization property plays a central role in the design of programming languages based on proof search, and more generally in the proof theory of linear logic. We present here a sequent calculus for non-commutative logic (NL) which enjoys the focalization property. In the multiplicative case, we give a focalized sequentialization theorem, and in the general case, we show that our focalized sequent calculus is equivalent to the original one by studying the permutabilities of rules for NL and showing that all permutabilities of linear logic involved in focalization can be lifted to NL permutabilities. These results are based on a study of the partitions of partially ordered sets modulo entropy.

Details DOI

LPAR Conference 1999 Conference Paper

Fucusing and Proof-Nets in Linear and Non-commutative Logic

Jean-Marc Andreoli
Roberto Maieli

Abstract Linear Logic [ 4 ] has raised a lot of interest in computer research, especially because of its resource sensitive nature. One line of research studies proof construction procedures and their interpretation as computational models, in the “Logic Programming” tradition. An efficient proof search procedure, based on a proof normalization result called “Focusing”, has been described in [ 2 ]. Focusing is described in terms of the sequent system of commutative Linear Logic, which it refines in two steps. It is shown here that Focusing can also be interpreted in the proof-net formalism, where it appears, at least in the multiplicative fragment, to be a simple refinement of the “Splitting lemma” for proof-nets. This change of perspective allows to generalize the Focusing result to (the multiplicative fragment of) any logic where the “Splitting lemma” holds. This is, in particular, the case of the Non-Commutative logic of [ 1 ], and all the computational exploitation of Focusing which has been performed in the commutative case can thus be revised and adapted to the non commutative case.

Details