Subnets of proof-nets in multiplicative linear logic with MIX

1997 ◽  
Vol 7 (6) ◽  
pp. 663-669 ◽  
Author(s):  
GIANLUIGI BELLIN
Keyword(s):  
Linear Logic ◽  
First Order ◽  
Correctness Criterion ◽  
Order Case ◽  
Proof Nets ◽  
Concurrent Processes ◽  
Propositional Constants ◽  
Intuitionistic Linear Logic ◽  
General Method

This paper studies the properties of the subnets of a proof-net for first-order Multiplicative Linear Logic without propositional constants (MLL−), extended with the rule of Mix: from [vdash ]Γ and [vdash ]Δ infer [vdash ]Γ, Δ. Asperti's correctness criterion and its interpretation in terms of concurrent processes are extended to the first-order case. The notions of kingdom and empire of a formula are extended from MLL− to MLL−+MIX. A new proof of the sequentialization theorem is given. As a corollary, a system of proof-nets is given for De Paiva and Hyland's Full Intuitionistic Linear Logic with Mix; this result gives a general method for translating Abramsky-style term assignments into proof-nets, and vice versa.

Concurrent programming as proof net construction

1998 ◽  
Vol 8 (6) ◽  
pp. 681-710
Author(s):  
G. PERRIER
Keyword(s):  
Proof Theory ◽  
Linear Logic ◽  
Concurrent Programming ◽  
Process Calculus ◽  
Concurrent Process ◽  
First Order ◽  
Proof Nets ◽  
Intuitionistic Linear Logic

We propose a concurrent process calculus, called Calcul Parallèle Logique (CPL), based on the paradigm of computation as proof net construction in linear logic. CPL uses a fragment of first-order intuitionistic linear logic where formulas represent processes and proof nets represent successful computations. In these computations, communication is expressed in an asynchronous way by means of axiom links. We define testing equivalences for processes, which are based on a concept of interface, and use the power of proof theory in linear logic.

scholarly journals Proof nets for multiplicative cyclic linear logic and Lambek calculus

2019 ◽  
Vol 29 (06) ◽  
pp. 733-762
Author(s):  
V. Michele Abrusci ◽  
Roberto Maieli
Keyword(s):  
Linear Logic ◽  
Lambek Calculus ◽  
Correctness Criterion ◽  
Proof Nets ◽  
Technical Achievement ◽  
Cyclic Fragment

AbstractThis paper presents a simple and intuitive syntax for proof nets of the multiplicative cyclic fragment (McyLL) of linear logic (LL). The main technical achievement of this work is to propose a correctness criterion that allows for sequentialization (recovering a proof from a proof net) for all McyLL proof nets, including those containing cut links. This is achieved by adapting the idea of contractibility (originally introduced by Danos to give a quadratic time procedure for proof nets correctness) to cyclic LL. This paper also gives a characterization of McyLL proof nets for Lambek Calculus and thus a geometrical (i.e., non-inductive) way to parse phrases or sentences by means of Lambek proof nets.

Causal dependencies in multiplicative linear logic with MIX

1995 ◽  
Vol 5 (3) ◽  
pp. 351-380 ◽  
Author(s):  
Andrea Asperti
Keyword(s):  
Distributed Systems ◽  
Linear Logic ◽  
Correctness Criterion ◽  
Proof Nets ◽  
Original Interpretation ◽  
Flow Of Information

A new correctness criterion for discriminating Proof Nets among Proof Structures of Multiplicative Linear Logic with the MIX rule is provided. This criterion is inspired by an original interpretation of Proof Structures as distributed systems, and logical formulae as processes. The computation inside a system corresponds to the logical flow of information inside a proof, that is, roughly speaking, a distributed version of Girard's token trip. Proof Nets are then characterised as deadlock free Proof Structures (deadlock free distributed systems). This result follows by explicitly considering the causal dependencies among logical formulae inside proofs, and it provides a new understanding of notions such as acyclicity, chains and empires in terms of concurrent computations.

scholarly journals Proofs, denotational semantics and observational equivalences in Multiplicative Linear Logic

2007 ◽  
Vol 17 (2) ◽  
pp. 341-359 ◽  
Author(s):  
MICHELE PAGANI
Keyword(s):  
Linear Logic ◽  
Denotational Semantics ◽  
Cut Elimination ◽  
Relational Semantics ◽  
Observational Equivalence ◽  
Proof Nets ◽  
General Method

We study full completeness and syntactical separability of MLL proof nets with the mix rule. The general method we use consists of first addressing these two questions in the less restrictive framework of proof structures, and then adapting the results to proof nets.At the level of proof structures, we find a semantical characterisation of their interpretations in relational semantics, and define an observational equivalence that is proved to be the equivalence induced by cut elimination. Hence, we obtain a semantical characterisation (in coherent spaces) and an observational equivalence for the proof nets with the mix rule.

A new correctness criterion for the proof nets of non-commutative multiplicative linear logics

2001 ◽  
Vol 66 (4) ◽  
pp. 1524-1542 ◽  
Author(s):  
Misao Nagayama ◽  
Mitsuhiro Okada
Keyword(s):  
Linear Time ◽  
Linear Logic ◽  
Time Algorithm ◽  
Affirmative Answer ◽  
Correctness Criterion ◽  
Correctness Checking ◽  
Proof Nets ◽  
Open Question

Abstract.This paper presents a new correctness criterion for marked Danos-Reginer graphs (D-R graphs, for short) of Multiplicative Cyclic Linear Logic MCLL and Abrusci's non-commutative Linear Logic MNLL.As a corollary we obtain an affirmative answer to the open question whether a known quadratic-time algorithm for the correctness checking of proof nets for MCLL and MNLL can be improved to linear-time.

Multiple conclusion linear logic: cut elimination and more

2020 ◽  
Vol 30 (1) ◽  
pp. 157-174 ◽  
Author(s):  
Harley Eades III ◽  
Valeria de Paiva
Keyword(s):  
Sequent Calculus ◽  
Linear Logic ◽  
Direct Proof ◽  
Cut Elimination ◽  
Tensor Model ◽  
Double Negation ◽  
Proof Nets ◽  
Small Change ◽  
Definition Of ◽  
Intuitionistic Linear Logic

Abstract Full intuitionistic linear logic (FILL) was first introduced by Hyland and de Paiva, and went against current beliefs that it was not possible to incorporate all of the linear connectives, e.g. tensor, par and implication, into an intuitionistic linear logic. Bierman showed that their formalization of FILL did not enjoy cut elimination as such, but Bellin proposed a small change to the definition of FILL regaining cut elimination and using proof nets. In this note we adopt Bellin’s proposed change and give a direct proof of cut elimination for the sequent calculus. Then we show that a categorical model of FILL in the basic dialectica category is also a linear/non-linear model of Benton and a full tensor model of Melliès’ and Tabareau’s tensorial logic. We give a double-negation translation of linear logic into FILL that explicitly uses par in addition to tensor. Lastly, we introduce a new library to be used in the proof assistant Agda for proving properties of dialectica categories.

Minimality of the correctness criterion for multiplicative proof nets

1998 ◽  
Vol 8 (6) ◽  
pp. 543-558 ◽  
Author(s):  
DENIS BECHET
Keyword(s):  
Linear Logic ◽  
Cut Elimination ◽  
Correctness Criterion ◽  
Proof Nets ◽  
Static Criterion

Almost a decade ago, Girard invented linear logic with the notion of a proof-net. Proof-nets are special graphs built from formulas, links and boxes. However, not all nets are proof-nets. First, they must be well constructed (we say that such graphs are proof-structures). Second, a proof-net is a proof-structure that corresponds to a sequential proof. It must satisfy a correctness criterion. One may wonder what this static criterion means for cut-elimination. We prove that every incorrect proof-structure (without cut) can be put in an environment where reductions lead to two kinds of basically wrong configurations: deadlocks and disconnected proof-structures. Thus, this proof says that there does not exist a bigger class of proof-structures than proof-nets where normalization does not lead to obviously bad configurations.

scholarly journals A fine-grained computational interpretation of Girard’s intuitionistic proof-nets

2022 ◽  
Vol 6 (POPL) ◽  
pp. 1-28
Author(s):  
Delia Kesner
Keyword(s):  
Linear Logic ◽  
Operational Semantics ◽  
Functional Term ◽  
Strong Normalization ◽  
Fine Grained ◽  
Fundamental Properties ◽  
Structural Equivalence ◽  
Proof Nets ◽  
Intuitionistic Linear Logic ◽  
Single Exponential

This paper introduces a functional term calculus, called pn, that captures the essence of the operational semantics of Intuitionistic Linear Logic Proof-Nets with a faithful degree of granularity, both statically and dynamically. On the static side, we identify an equivalence relation on pn-terms which is sound and complete with respect to the classical notion of structural equivalence for proof-nets. On the dynamic side, we show that every single (exponential) step in the term calculus translates to a different single (exponential) step in the graphical formalism, thus capturing the original Girard’s granularity of proof-nets but on the level of terms. We also show some fundamental properties of the calculus such as confluence, strong normalization, preservation of β-strong normalization and the existence of a strong bisimulation that captures pairs of pn-terms having the same graph reduction.

Towards the Temporal Approach to Abstract Data Types

1988 ◽  
Vol 11 (1) ◽  
pp. 49-63
Author(s):  
Andrzej Szalas
Keyword(s):  
Temporal Logic ◽  
Abstract Data Types ◽  
Data Types ◽  
First Order ◽  
Abstract Data ◽  
Order Completeness ◽  
General Method

In this paper we deal with a well known problem of specifying abstract data types. Up to now there were many approaches to this problem. We follow the axiomatic style of specifying abstract data types (cf. e.g. [1, 2, 6, 8, 9, 10]). We apply, however, the first-order temporal logic. We introduce a notion of first-order completeness of axiomatic specifications and show a general method for obtaining first-order complete axiomatizations. Some examples illustrate the method.

Sign in / Sign up

Export Citation Format

Share Document