In this paper we explore the design of sequent calculi operating on graphs. For this purpose, we introduce a set of logical connectives extending the well-known correspondence between classical propositional formulas and cographs, and we define sequent systems operating on formulas over these connectives.

We prove, using an analyticity argument based on cut-elimination, that our systems provide conservative extensions of multiplicative linear logic (without and with mix) and classical propositional logics. We conclude by showing that one of our systems captures graph isomorphism as logical equivalence, and that this system is also sound and complete for the graphical logic $\GS$.

§ INTRODUCTION

In theoretical computer science, formulas play a crucial role in describing complex abstract objects.
At the syntactical level, the formulas of a logic describe complex structures by means of unary and binary operators, usually thought of as connectives and modalities respectively.
On the other hand, graph-based syntaxes are often favored in formal representation, as they provide an intuitive and canonical description of properties, relations and systems.
By means of example, consider the two graphs below:

\va1\qquad \vb1 \qquad \vc1 \qquad \vd1
\Dedges{b1/a1,b1/c1,d1/c1}
\qquad\quor\qquad
\va1\qquad \vb1 \qquad \vc1 \qquad \vd1
\Gedges{b1/a1,b1/c1,d1/c1}

It follows from results in [62, 21] that describing any of the above graphs by means of formulas only employing binary connectives would require repeating at least one vertex.
As a consequence, formulas describing complex graphs are usually long and convoluted, and a specific encodings are needed to standardize such formulas.

Since graphs are ubiquitous in theoretical computer science and its applications,
a natural question to ask is whether it is possible to define formalisms having graphs, instead of formulas, as first-class terms of the syntax.
Such a paradigm shift would allow to design efficient automated tools free from the bureaucracy introduced to handle the encoding required to represent graphs.
At the same time, a graphical syntax would provide a useful tool for investigations such as the ones in [63] or [27, 25], where the authors restrain their framework to sequential-parallel orders, as these can be represented by means of formulas with at most binary connectives.

Two recent lines of works have generalized proof theoretical methodologies to graphs, extending the correspondence between classical propositional formulas and cographs.
In these works, systems operating on graphs are defined via local and context-free rewriting rules, similarly as what done in deep inference systems [33, 34, 9].
The first line of research, carried out by Calk, Das, Rice and Waring in various works [18, 17, 64, 23, 24], explores the use of maximal stable sets/cliques-preserving homomorphisms to define notions of entailment[
A similar approach was proposed in [56] for studying pomsets.
], and study the resulting proof theory.
Here, the choice of the using of a deep inference formalism is natural, since the rules of the calculus are local rewritings.

The second line of research, investigated by the author, Horne, Mauw and Straßburger in several contributions [4, 5, 2], studies the (sub-)structural proof theory of arbitrary graphs, with an approach inspired by linear logic [29] and deep inference [33].
The main goal of this line of research, partially achieved with the system $\GVsl$ operating on mixed graphs [2], is to obtain a generalization of the completeness result of the logic $\BV$ with respect to pomset inclusion.
The logic $\BV$ contains a non-commutative binary connective $\lseq$ allowing to represent series-parallel partial order multisets as formulas in the syntax (as in Retoré's $\pomset$ logic [57]), and to capture order inclusion as logical implication. However, as shown in [60], no cut-free sequent system for $\BV$ can exists – therefore neither for $\pomset$ logic, which strictly contains it [54, 53].
For this reason the aforementioned line of work focused on deep inference systems, and the question about the existence of a cut-free sequent calculus for $\GS$ (the restriction of $\GVsl$ on undirected graphs originally defined in [4]) was left open.

Main contributions

In this paper we focus on the definition of sequent calculi for graphical logics, and we positively answer the above question by providing, among other results, a cut-free sound and complete sequent calculus for $\GS$.
By using standard techniques in sequent calculus, we thus obtain a proof of analiticity for this logic which is simpler and more concise with respect to the one in [5].

To achieve these results, we introduce graphical connectives, which are operators that can be naturally interpreted as graphs.
We then define the sequent calculi $\PML$, $\PMLx$ and $\PLK$, containing rules to handle these connectives.
After showing that cut-elimination holds for these systems,
we prove that  $\PML$, $\PMLx$ and $\PLK$ define conservative extensions of multiplicative linear logic, multiplicative linear logic with mix and classical propositional logic respectively.
We then prove that formulas interpreted as the same graph are logically equivalent, thus justifying the fact that we consider these systems as operating on graphs rather than formulas.

We conclude by showing that $\PMLx$ is sound and complete with respect to the logic $\GS$, thus providing a simple sequent calculus for the logic.

Outline of the paper

In <Ref> we recall definitions and results in graph theory and the notion of modular decomposition.
In <Ref> we use these notions to extend the correspondence between classical propositional formulas and cographs to any graph.
We define linear sequent calculi and we prove their properties.
In <Ref> we show that one of these calculi is sound and complete with respect to the set of non-empty graphs provable in the deep inference system $\GS$ studied in [4, 5].

In <Ref> we define a proof system which is a conservative extension of classical logic.

To conclude, we summarize in <Ref> some of the possible the research directions opened by this work.

§ FROM FORMULAS TO GRAPHS

In this section we recall standard results from the literature on graphs such as modular decomposition and cographs.
We then introduce the notion of graphical connectives
allowing us to extend the correspondence between cographs and classical propositional formulas to general graphs.

§.§ Graphs and Modular Decomposition

In this work are interested in using graphs to represent patterns of interactions by means of the binary relations (edges) between their components (vertices).

For this reason we recall the definition of
labeled graph (the mathematical structure we use to encode these patterns)
together with
the definition of
isomorphism (the standard notion of identity on labeled graphs)
the rougher notion of similarity (equivalence up-to labels over vertices).

A $\litset$-labeled graph (or simply graph)
is given by
a finite set of vertices $\vG$,
a partial labeling function
$\labsymb_\gG\colon \vertices[\gG]\to \litset$
associating a label $\lab v$ from a given set of labels $\litset$ to each vertex $v\in\vG$
(we may represent $\labsymb_\gG$ as a set of equations of the form $\lab v= \ell_v $ and denote by $\emptyset$ the empty function),
a non-reflexive symmetric edge relation $\uG\subset\vof\gG\times\vof\gG$ whose elements, called edges, may be denoted $vw$ instead of $(v,w)$.

The empty graph $\tuple{\emptyset,\emptyset,\emptyset}$ is denoted $\emptygraph$.

A similarity between two graphs $\gG$ and $\gG'$
is a bijection
$f\colon \vG \to \vof{\gG'}$
such that
$x\uedge[\gG] y$ iff $f(x)\uedge[\gG'] f(y) $
for any $x,y\in\vG$.

An  isomorphism is a similarity $f$ such that $\lab{v}=\lab{f(v)}$ for any $x,y\in\vG$.

Two graphs
$\gG$ and $\gG'$ are
similar (denoted $\gG\isym\gG'$)
if there is an similarity between $\gG$ and $\gG'$.
A symmetry is a similarity of a graph with itself.

They are
isomorphic (denoted $\gG=\gG'$)
if there is a isomorphism between $\gG$ and $\gG'$.
From now on, we consider two isomorphic graphs to be the same graph.

Two vertices $v$ and $w$ in $\gG$ are connected
if there is a sequence  $v=u_0,\ldots, u_n=w$  of vertices in $\gG$ (called path)
such that $u_{i-1}\uedge[\gG]u_{i}$ for all $i\in\intset1n$.
A connected component of $\gG$ is a maximal set of connected vertices in $\gG$.

A graph $\gG$ is a clique (resp. a stable set)
$\nuedge[\gG]=\emptyset$ (resp. $\uG=\emptyset$).

When drawing a graph or an unlabeled graph
we draw $\vv1\quad\vw1\Gedges{v1/w1}$ whenever $v\uedge w$,
we draw no edge at all whenever $v\nuedge w$.
We may represent a vertex of a graph by using its label instead of its name.
For example, the single-vertex graph $\gG=\tuple{\set{v},\lG,\emptyset}$ may be represented either by a the vertex name $\vv1$ or by the vertex label $\lab v$ (or $\bullet$ if $\lab v $ is not defined).

Note that,
since we are considering isomorphic graphs to be the same,
as soon as there is no ambiguity due to vertices represented by the same symbol,
we can assume
the representation of a graph to provide us one of the possible triple (set of vertices, label function, and set of edges) defining it.

Consider the following graphs:

\gF	&	\Tuple{\Set{u_1,u_2,u_3,u_4},\Set{\lab{u_1}=a,\lab{u_2}=b,\lab{u_3}=c,\lab{u_4}=d},\Set{u_1u_2,u_2u_3,u_3u_4}}
\\
\gG	&	\Tuple{\Set{v_1,v_2,v_3,v_4},\Set{\lab{v_1}=b,\lab{v_2}=a,\lab{v_3}=c,\lab{v_4}=d},\Set{v_1v_2,v_1v_3,v_3v_4}}
\\
\gH	&	\Tuple{\Set{w_1,w_2,w_3,w_4},\Set{\lab{w_1}=a,\lab{w_2}=b,\lab{w_3}=c,\lab{w_4}=d},\Set{w_1w_2,w_1w_3,w_3w_4}}
\end{array}

They are all symmetric, that is $\gF\isym\gG\isym\gH$, but $\gF=\gG\neq \gH$ as can easily be verified using their representations:

\gF=\va1\quad\vb1\quad\vc1\quad\vd1\Gedges{a1/b1,b1/c1,c1/d1}=\gG
\qquand
\gH=\vb1\quad\va1\quad\vc1\quad\vd1\Gedges{b1/a1,a1/c1,c1/d1}

The problem of graph isomorphism is a standard $\NP$-problem (to be more precise, its complexity is quasi-polynomial [12]).
That is, verify that a given bijection between the sets of vertices of two graphs is an isomorphism can be checked in polynomial time,
while there is no known polynomial time algorithm to find such an isomorphism.
For this reason, whenever we say that two graphs are the same, either we assume they share the same set of vertices, therefore implicitly assuming the isomorphism $f$ to be defined by the identity function over the set of vertices, or we assume an isomorphism to be given.
This allows us to verify whether two graphs are the same in polynomial time.

In order to use proof theoretical methodologies on graphs, we need a suitable notion of subgraphs to be used in the same way sub-formulas are used in proof systems, that is, to state properties of the calculus or to define the behavior of rules.
For this purpose, we use for a notion of  module to identify subgraph allowing us to decompose a graph using abstract syntax trees similar to the ones underlying formulas [28, 42, 37, 46, 49, 26].
A module is a subset of vertices of a graph having the same edge-relation with any vertex outside the subset.
This definition generalizes the interaction we usually be observed in formulas, where, in the formula tree, any literal in a subformula has the same relation (the one given by the least common ancestor) with a given literal not occurring in the subformula itself.

Let $\gG=\tuple{\vG,\lG,\eG}$ be a graph and $W\subseteq\vG$.
The graph induced by $W$ is
the graph
$\gG\restr{W}\coloneqq\Tuple{W,\lG\restr{W},\uG\cap\left(W\times W\right)}$
$\lG\restr{W}(v)\coloneqq \lG(v)$ for all $v\in W$.

A module of a graph $\gG$ is a subset $M$ of $\vG$ such that
$x\uedge z$ iff $ y\uedge z $
for any $x,y\in M$,
$z\in \vG \setminus M$.
A module $M$ is trivial if $M=\emptyset$,
$M=\vG$, or $M=\set{x}$ for some $x\in\vG$.

From now on, we identify a module $\gM$ of a graph $\gG$ with
the induced subgraph $\gG\restr{M}$.

A connected component of a graph $\gG$ is a module of $\gG$.

Using modules we can optimize the way we represent graphs reducing the number of edges drawn without losing information, relying on the fact that all vertices of a module has the same edge-relation with any vertex outside the module.

In representing graphs we may border vertices of a same module by a closed line.
An edges connected to such a closed line denotes the existence of an edge to each vertex inside it.
By means of example, consider the following graph and its more compact modular representation.

\begin{equation}
\begin{array}{c@{\qquad}c@{\qquad}c}
\va1&\vc1
\\
\\
\vb1&\vd1
\end{array}
\Gedges{a1/b1,a1/c1,a1/d1,b1/d1,b1/c1,e1/c1,e1/d1}
\qquad=\qquad
\vmod1{\begin{array}{c}\va1\\\\\vb1\end{array}}\quad\vmod2{\begin{array}{c}\vc1\\\\\vd1\end{array}}\quad \ve1
\Gedges{a1/b1,mod1/mod2,mod2/e1}
\end{equation}

The notion of module is related to a notion of context, which can be intuitively formulated as a graph with a special vertex playing the role of a hole in which we can plug in a module.

A context $\cC\conso$ is a (non-empty) graph containing a single occurrence of a special vertex $\chole$ (such that $\lab\chole$ is undefined).
It is trivial if $\cC\conso=\chole$.

If $\cC\conso$ is a context and $\gG$ a graph, we define $\cC\cons{\gG}$ as the graph obtained by replacing $\chole$ by $\gG$.

\begin{equation*}
\cC\cons\gG
\coloneqq
\Tuple{
%			\;
\left(\vertices[\cC\conso]\setminus\set{\chole}\right)\uplus \vG
\;,\;
\labsymb_\cC\cup\lG
\;,\;
\Set{vw\mid v,w\in \vertices[\cC\conso]\setminus\set{\chole}, v\uedge[\cC\conso]w}
\cup
\Set{
\mid
v\in \vertices[\cC\conso]\setminus\set{\chole},
%			\;
\end{equation*}

A set of vertices $\gM$ is a module of a graph $\gG$
there is a context $\cC\conso$ such that $\gG=\cC\cons{\gM}$.

We generalize this idea of replacing a vertex of a graph with a module
by defining the operations of composition-via a graph, where all vertices of a graph are replaced in a “modular way” by modules.

Let $\gG$ be a graph with $\vof\gG=\set{v_1,\ldots,v_n}$
let $\gH_1,\ldots,\gH_n$ be graphs.

We define the
composition of $\gH_1,\ldots,\gH_n$ via $\gG$
as the graph $\gG\connn{\gH_1,\ldots,\gH_n}$
obtained by replacing each vertex $v_i$ of $\gG$
with a module $\gH_i$ for all $i\in\intset1n$.

\begin{equation}\label{eq:compVia}
\gG\connn{\gH_1,\ldots,\gH_n}
\;=\;
\Tuple{
\;
\biguplus_{i=1}^n\vof{\gH_i}
\;,\;
\bigcup_{i=1}^n{\labsymb_{\gH_i}}
\;,\;
\left(\bigcup_{i=1}^n\uedge[\gH_i]\right)
\cup
\Set{\!\!
\begin{array}{c|c}
x\in \vof{\gH_i},
v_i\uedge[\gG] v_j
\end{array}\!\!
\;
\end{equation}

The subgraphs $\gH_1,\ldots, \gH_n$ are called factors of $\gG\connn{\gH_1,\ldots, \gH_n}$

and, by definition,
are (possibly not maximal) modules of $\gG\connn{\gH_1,\ldots, \gH_n}$.

The information about the labels of the graph $\gG$ used to define the composition-via operation is lost.
if $\gG$ is a graph with $\vG=\set{v_1,\ldots, v_n}$ and
$\sigma$ a permutation over the set $\intset1n$
such that
the map $f_\sigma:\vG\to\vG$ mapping $v_i$ in $f_\sigma(v_i)=v_{\sigma(i)}$ for all $i\in\intset1n$ is an similarity between $\gG$ and $\gG$,
then $\gG\connn{\gH_1,\ldots,\gH_n}=\gG'\connn{\gH_1,\ldots,\gH_n}$.

In order to establish a connection between graphs and formulas, from now on we only consider graphs whose set of labels belong to the set
$\labelset=\Set{a,\cneg a\mid a\in\atomset}$ where $\atomset$ is a fixed set of propositional variables.
We then define the dual of a graphs.

Let $\gG=\tuple{\vG,\lG,\eG}$ be a graph.
We define the edge relation $\nuG\coloneqq\Set{(v,w)\mid v\neq w \mbox{ and } vw\notin\uG}$
we define the dual graph of $\gG$ as the graph
$\nG\coloneqq \Tuple{\vG,\nuedge[\gG],\lnG}$ with $\lnG(v)=\cneg{\left(\lG(v)\right)}$ (assuming $\cnegneg a=a$ for all $a\in\atomset$).

By definition, each module of a graph corresponds to a module of its dual graph.
It follows that a connected component of $\nG$ is a module of $\gG$.

If $\mathcal G$ is the representation of a graph $\gG$,
then we may represent the graph $\nG$  by bordering the representation of $\gG$ with a closed line with the negation symbol on the upper-right corner, that is,  $\cneg{\vmod1{\mathcal G}}$.

§.§ Classical Propositional Formulas and Cographs

The set of classical (propositional) formulas is generated from a set of propositional variable $\atomset$  using the negation $\cneg{(\cdot)}$, the disjunction $\lor$ and the conjunction $\land$
using the following grammar:

\begin{equation}\label{eq:LKform}
\fA,\fB			\coloneqq
a 				\mid
\fA \lor \fB 	\mid
\fA \land \fB 	\mid
\cneg\fA
\qquad
\mbox{with $a\in\atomset$.}
\end{equation}

We denote by $\feq$  the equivalence relation over formulas generated by the following laws:

\begin{equation}\label{eq:formEQ}
\begin{array}{rl}
\mbox{\defn{Equivalence laws}}
\left\{\begin{array}{r@{\;\feq\;}l@{\hskip4em}r@{\;\feq\;}l}
\fA \lor \fB			&\fB\lor \fA
\fA \lor (\fB\lor \fC)	&(\fA\lor \fB)\lor \fC
\\
\fA \land \fB			&\fB\land \fA
\fA \land (\fB\land \fC)&(\fA\land \fB)\land \fC
\end{array}\right.
\\[8pt]
\mbox{\defn{De-Morgan laws}}
\;\left\{
\begin{array}{r@{\;\feq\;}l@{\hskip6.8em}r@{\;\feq\;}l}
\!\cneg{(\cneg \fA)}		&\fA
\cneg{(\fA\land\fB)}	&\cneg \fA \lor \cneg\fB
\end{array}
\right.
\end{array}
\end{equation}

We define a map from literals to single-vertex graphs, which extends to formulas via the composition-via
the unlabeled
two-vertices stable set $\stable2$
two-vertices clique $\clique2$.

Let $\fA$ be a classical formula, then $\gof \fA$ is the graph inductively defined as follows:

\gof a = a
\qquad
\gof {\cneg \fA} = \cneg{\gof\fA}
\qquad
\gof {\fA\lor\fB} = \stable2\Connn{\gof\fA , \gof\fB}
\qquad
\gof {\fA\land\fB} = \clique2\Connn{\gof\fA , \gof\fB}

where $\stable2$ and $\clique{2}$ are respectively a stable set and a clique with $2$ vertices,
where we denote by $a$ the single-vertex graph, whose vertex is labeled by $a$.

We can easily observe that the map $\gof\cdot$ well-behaves with respect to the equivalence over formulas $\feq$, that is, equivalent formulas are mapped to the symmetric graphs.

Let $\fA$ and $\fB$ be classical formulas.
Then $\fA\feq\fB$ iff $\gof\fA\greq\gof\fB$.

We finally recall the definition of cographs, and the theorem establishing the relation between cographs and classical formulas, i.e., providing an alternative definition of cographs as graphs generated by single-vertex graphs using the composition-via a two-vertices no-edge graph and a two-vertices one-edge graph.

A cograph is a graph $\gG$ such that
there are no four vertices $v_1,v_2,v_3,v_4$ in $\gG$
such that the induced subgraph $\gG\restr{\set{v_1,v_2,v_3,v_4}}$ is similar to the graph $\tuple{\set{a,b,c,d},\emptyset,\set{ab,bc,cd}}=\va1\quad\vb1\quad\vc1\quad\vd1\Gedges{a1/b1,b1/c1,c1/d1}$ .

A graph $\gG$ is a cograph iff there is a formula $\fA$ such that $\gG\isym\gof{\fA}$.

§.§ Modular Decomposition of Graphs

We recall the notion of prime graph,
allowing us to provide canonical representatives of graphs via modular decomposition.
(see e.g., [28, 42, 37, 46, 49, 26]).

A graph $\gG$ is prime if $\sizeof{\vG}> 1$ and all its modules are trivial.

We recall the following standard result from the literature.

Let $\gG$ be a graph with at least two vertices.
Then there are non-empty modules $ \gM_1, \dots, \gM_n $ of $\gG$ and a prime graph $\gP$ such that $\gG=\gP\connn{\gM_1, \dots, \gM_n}$.

This result implies the possibility of describing graphs using single-vertex graphs and the operation of composition-via prime graphs.
More precisely, we can define the notion of modular decomposition of a graph composition-via prime graphs to provide a more canonical representation.

Let $\gG$ be a non-empty graph.
A modular decomposition of $\gG$ is a way to write $\gG$ using single-vertex graphs and the operation of composition-via prime graphs:

* if $\gG$ is a graph with a single vertex $x$ labeled by $a$, then $\gG=a$
(i.e., $\gG=\tuple{\set{x},\lab{x}=a,\emptyset}$);

* if $\gH_1, \ldots, \gH_n$ are maximal modules of $\gG$ such that $\vertices[\gG]=\biguplus_{i=1}^n\vertices[\gH_i]$,
then there is a unique prime graph $\gP$ such that $\gG=\gP\connn{\gH_1, \ldots, \gH_n}$.

There are various reasons why modular decomposition is not unique.

The first is due to the possible presence of cliques and stable sets.

By means of example, consider a clique with three vertices $u$, $v$ and $w$
can be represented as $(u \ltens v)\ltens w$ or $u\ltens(v\ltens w)$.

We already observed the second reason in <Ref>,
since graph symmetries allow us to represent the same graph by different decompositions,
as shown in top-most modular decomposition below on the left.

\begin{array}{cc}
\gP\connn{u,v,w,t}=\vu1\quad\vv1\quad\vw1\quad\vt1\Gedges{u1/v1,v1/w1,w1/t1}=\gP\connn{t,w,v,u}
\\
\gP\connn{u,v,w,t}=\vu1\quad\vv1\quad\vw1\quad\vt1\Gedges{u1/v1,v1/w1,w1/t1}=\gP'\connn{u,w,v,t}
\end{array}
\quad\mbox{where}\quad
\gP =\va1\quad\vb2\quad\vc3\quad\vd4\Gedges{a1/b2,b2/c3,c3/d4}
\quand
\gP'=\va1\quad\vc3\quad\vb2\quad\vd4\Gedges{a1/c3,b2/c3,b2/d4}
\;.

Finally, two symmetric prime graphs could provide distinct modular decompositions of the same graph,
as shown above with symmetric prime graphs $\gP$ and $\gP'$.

The first problem could be addressed by considering in the modular decomposition not only prime graphs, but also cliques and stable sets, that is, including $n$-ary versions of the operations $\lpar$ and $\ltens$.
We show later in this paper that this problem is irrelevant due to the associativity of $\lpar$ and $\ltens$.
The second problem cannot be addressed without enforcing a cumbersome order over graphs taking into account vertex labels and factor positions.
However, we can address the latter source of ambiguity by introducing the notion of base of graphical connectives,
allowing us to provide a single canonical prime graph for each class of symmetric prime graphs.

A graphical connective
(with arity $n=\sizeof\vC$)
is given by
a finite list of vertices $\vC=\tuple{v_1,\ldots,v_n}$
a non-reflexive symmetric edge relation $\uC$ over the set of vertices occurring in $\vC$.

We denote by $\gG_\gC$ the graph corresponding to $\gC$,
that is, the graph $\gG_\gC=\tuple{\set{v\mid v \mbox{ in } \vC},\emptyset,\uC}$.
The composition-via a graphical connective
is defined as the composition-via the graph $\gG_\gC$.

A graphical connective is prime
if $\gG_\gC$ is a prime graph.
A set $\primesign$ of prime graphical connectives  is a base
if for each prime graph $\gP$

there is a unique connective $\gC\in\primesign$
such that $\gP\sim \gG_\gC$.

Given an $n$-ary connective $\gC$,
we define the following sets of permutations over the set $\intset1n$:

\begin{equation}
\begin{array}{l@{\;:\;}c@{\quad\coloneqq\quad}l}
\mbox{the \defn{group\footnote{
It can be easily shown that $\permset n$
%					contains the the identity permutation (denoted $\idperm$)
%					and
is subgroup of the group of permutations over the set $\intset1n$.
of symmetries} of $\gC$}&
\Sym{\gC}	&
\Set{\;\sigma\mid \gC\connn{a_1,\ldots, a_n}\greq\gC\connn{a_{\sigma(1)},\ldots, a_{\sigma(n)}}}
\qquad
\\
\mbox{the \defn{set of dualizing symmetries} of $\gC$}&
\Dsym{\gC}	&
\Set{\;\sigma\mid \cneg{(\gC\connn{a_1,\ldots, a_n})}\greq\gC\connn{\cneg a_{\sigma(1)},\ldots, \cneg a_{\sigma(n)}}
\end{array}
\end{equation}

for any $a_1,\ldots, a_n$ single-vertex graphs.

We define the following graphical connectives (with $n>1$):

\begin{equation}\label{eq:gCon}
\begin{array}{r@{\coloneqq}l@{\;=\;}c}
\lpar\connn{v_1,v_2}
\Tuple{\tuple{v_1,v_2},\emptyset}
\vmod1{\vind1\quad \vind2}
\\[5pt]
\ltens\connn{v_1,v_2}
\Tuple{\tuple{v_1,v_2},\set{v_1v_2}}
\vmod2{\vind1 \quad \vind2 \Gedges{v1/v2}}
\\[5pt]
\gPath n\connn{v_1,\ldots,v_n}
\Tuple{\tuple{v_1,\ldots, v_n},\set{v_iv_{i+1}\mid i\in\intset1{n-1}}}
\vmod1{\vind1\quad\vind2\quad \vgdots1 \quad\vind{n-1}\quad\vind n
\Gedges{v1/v2,v2/gdots1,gdots1/vn-1,vn-1/vn}}
\\[5pt]
\Pbull\connn{v_1,\ldots, v_5}
\Tuple{\tuple{v_1,\ldots, v_5},\set{(v_1v_2,v_2v_3,v_3v_4,v_5v_2,v_5v_3)}}
\vmod1{
\begin{array}{c@{\quad}ccc@{\quad}c}
\vind1&\vind2&&\vind3&\vind4
\\
\end{array}
\Gedges{v1/v2,v2/v3,v3/v4}
\Gedges{v5/v2/20,v3/v5/20}
\end{array}
\end{equation}

Consider the following graph $\gG$ and its dual $\nG$:

\gG=
\begin{array}{cc}
\begin{array}{c@{\qquad}c}&\vc1\\\vd1\end{array}
\begin{array}{c@{\qquad\qquad}c}\ve1\\&\vf1\end{array}
\\[10pt]
\begin{array}{c@{\qquad}c}\va1&\vb1\end{array}
\begin{array}{c@{\qquad}c@{\qquad}c}\vg1& \vh1& \vi1\end{array}
\end{array}
\Gedges{e1/f1,c1/d1}
\multiGedges{a1,b1}{c1,d1}
\multiGedges{c1,d1}{e1,f1}
\multiGedges{e1,f1}{g1,h1,i1}
\Gedges{g1/h1,i1/h1}
\bentGedges{i1/g1/20}
\qquand
\nG=
\begin{array}{c@{\qquad}c}
\begin{array}{c@{\quad}c}&\vnd1\\[-5pt]\vnc1\end{array}
\begin{array}{c@{\qquad}c}\vne1\\[-5pt]&\vnf1\end{array}
\\
\begin{array}{c@{\qquad}c}\vna1\\\\&\vnb1\end{array}
\begin{array}{c@{\quad}c@{\quad}c}&& \vni1 \\& \vnh1 \\ \vng1 \end{array}
\end{array}
\Gedges{na1/nb1}
\multiGedges{ng1,nh1,ni1}{nc1,nd1}
\multiGedges{na1,nb1}{ne1,nf1}
\multiGedges{na1,nb1}{ng1,nh1,ni1}

We can write them as

\begin{array}{l@{=}c@{=}c}
\gG
\Pfour\Connn{a\lpar b, c\ltens d,e\ltens f,g\ltens(h\ltens i)}
\vmod1{\va1\quad\vb1}
\quad
\vmod2{\vc1\quad\vd1}
\quad
\vmod3{\ve1\quad\vf1}
\quad
\vmod4{\vg1\quad \vmod5{\vh1\quad \vi1}}
\Gedges{e1/f1,c1/d1}
\Gedges{mod1/mod2,mod2/mod3,mod3/mod4}
\Gedges{g1/mod5,i1/h1}
\\
\nG
\nPfour\Connn{\cneg a\ltens \cneg b, \cneg c\lpar \cneg d,\cneg e\lpar \cneg f,\cneg g\lpar(\cneg h\lpar \cneg i)}
\\&
\Pfour\Connn{\cneg c\lpar \cneg d,\cneg a\ltens \cneg b, \cneg g\lpar(\cneg h\lpar \cneg i),\cneg e\lpar \cneg f}
\vmod3{\vne1\quad\vnf1}
\quad
\vmod1{\vna1\quad\vnb1}
\quad
\vmod4{\vng1\quad \vnh1\quad \vni1}
\quad
\vmod2{\vnc1\quad\vnd1}
\Gedges{na1/nb1}
\Gedges{mod1/mod3,mod2/mod4,mod1/mod4}
\end{array}

We can reformulate the standard result on modular decomposition as follows.

Let $\gG$ be a non-empty graph and $\primesign$ a base.

Then then there is a unique way (up to symmetries of graphical connectives and associativity of $\lpar$ and $\ltens$)
to write $\gG$ using single-vertex graphs and the graphical connectives in $\primesign$.

Two graphs are isomorphic iff they admit a same modular decomposition.

§.§ Graphs as Formulas

In order to represent graphs as formulas,
we define new connectives beyond conjunction and disjunction to represent graphical connectives in a base $\primesign$.
From now on, we assume bases $\primesign$ containing the graphical connectives in <Ref> to be fixed.

The set of  is generated by
the set of propositional atoms $\atomset$,
a unit $\funit$,

using the following syntax:

\begin{equation}
\fA_1,\ldots,\fA_n
\coloneqq
\funit	\mid
a 		\mid
\cneg a \mid
\con[\gP]\connn{\fA_1,\ldots, \fA_{n_\gP}}
\qquad
\mbox{with $a\in\atomset$ and $\gP \in\primesign$}
\end{equation}

We simply denote $\lpar$ (resp. $\ltens$)
the binary connective $\con[\lpar]$ (resp. $\con[\ltens]$)
we write
$\fA\lpar\fB$ instead of  $\con[\lpar]\connn{\fA,\fB}$
(resp. $\fA\ltens\fB$ instead of $\con[\ltens]\connn{\fA,\fB}$).

The arity of the connective $\con[\gP]$ is the arity $n_\gP$ of $\gP$.

A literal is a of the form $a$ or $\cneg a$ for an atom $a\in\atomset$.
The set of literals is denoted $\litset$.

A $\con$-formula is a with main connective $\con$, that is, a of the form $\con\connn{\fA_1, \ldots, \fA_n}$.

A is unit-free if it contains no occurrences of $\funit$ and
vacuous if it contains no atoms.
A is pure if non-vacuous and such that its vacuous subformulas are $\funit$.
A  is a formula containing only occurrences of $\lpar$ and $\ltens$ connectives.

A context formula (or simply context) $\fcC\conso$ is a formula containing an hole $\chole$ taking the place of an atom.

Given a context $\fcC\conso$, the formula $\fcC\cons\fA$ is defined by simply replacing the atom $\chole$ with the formula $\fA$.

For example, if $\fcC\conso=\fB\lpar (\chole\ltens \fC)$, then $\fcC\cons\fA=\fB\lpar ( \fA\ltens \fC)$.

For each $\fA$ formula (or context), the graph $\gof \fA$ is defined as follows:

\begin{equation}\label{def:gof}
\gof\chole = \chole
\qquad
\gof\funit = \emptygraph
\qquad
\gof a = a
\qquad
\gof {\cneg\fA} = \cneg{\gof\fA}
\qquad
\gof{\con[\gP]\connn{\fA_1,\ldots, \fA_n}}=
\gP\Connn{\gof{\fA_1},\ldots, \gof{\fA_n}}
\end{equation}

We could consider
a formula $\fA$ over the set of occurrences of literals $\set{\fx_1,\ldots ,\fx_n}$
as a synthetic connective.
That is,
we may denote by $\fA\connn{\fB_1,\ldots, \fB_n}$
the formula obtained by replacing each literal $x_i$ with a corresponding $\fB_i$ for all $i\in\intset1n$.

The set of symmetries of $\fA$ (denoted $\Sym{\fA}$) is the set of permutations $\sigma$ over $\intset1n$ such that $\gof{\fA\connn{\fx_1,\ldots ,\fx_n}}=\gof{\fA\connn{\fx_{\sigma(1)},\ldots ,\fx_{\sigma(n)}}}$.

The equivalence relation $\feq$ over formulas
is generated by the
following equations:

\begin{equation*}
\begin{array}{l@{\;}l}
\mbox{\defn{Equivalence laws}}
\left\{\begin{array}{l@{\quad}r@{\;\feq\;}l@{\quad}l}
%			\\[-20pt]
\con[\gP]\connn{\fA_1, \ldots,\fA_{\sizeof\gP}}
\con[\gP]\connn{\fA_{\sigma(1)},\ldots,\fA_{\sigma(\sizeof\vP)}}
\mbox{ for each }\sigma\in\Sym\gP
\\
\fA\ltens(\fB\ltens \fC)
(\fA\ltens\fB)\ltens \fC
\\
\fA\lpar(\fB\lpar \fC)
(\fA\lpar\fB)\lpar \fC
\end{array}\right.
\\\\
\mbox{\defn{De-Morgan laws}}
\left\{\begin{array}{l@{\quad}r@{\;\feq\;}l@{\;}l}
\multicolumn{4}{c}{
\cneg\funit
\;\feq\;
\funit
\qquad\qquad
\cnegneg \fA
\;\feq\;
\fA
\qquad
\\
\mbox{only if }\Dsym\gP=\emptyset:
\cneg{\left(\con[\gP]\connn{\fA_1,\ldots\fA_{n_\gP}}\right)}
\con[\cneg{\gP}]\connn{\cneg{\fA_{\sigma(1)}},\dots,\cneg{\fA_{\sigma(n_\gP)}}}
\\
\mbox{only if }\Dsym\gP\neq \emptyset:
\cneg{\left(\con[\gP]\connn{\fA_1,\ldots\fA_{n_\gP}}\right)}
\con[\gP]\connn{\cneg{\fA_{\rho(1)}},\dots,\cneg{\fA_{\rho(n_\gP)}}}
\mbox{ for each }\rho\in\Dsym\gP
\end{array}\right.
\end{array}
\end{equation*}

for each $\gP\in\primesign$ (with arity $n_\gP$).

The (linear) negation over formulas is defined by letting

\cneg \funit = \funit
\qquad
\cnegneg \fA= \fA
\qquad
\cneg{\left(\con[\gP]\connn{\fA_1,\ldots, \fA_n}\right)}
\con[\gQ]\connn{\cneg\fA_{\sigma_\gP(1)}, \ldots, \cneg\fA_{\sigma_\gP(n)}}
\quad

where $\gQ$ is the unique graphical connective in $\primesign$ such that $\gof{\con[\gP]\Connn{a_1,\ldots, a_n}}=\gQ\Connn{\cneg a_{\sigma(1)},\ldots, \cneg a_{\sigma_n}}$
for any single-vertex graphs $\cneg a_1,\ldots,\cneg a_n$ (with vertex labeled by $\cneg a_1,\ldots,\cneg a_n$ respectively)
a permutation $\sigma_\gP$ over the set $\intset1n$.
Note that the permutation $\sigma_\gP$ may be not unique.
This is not a problem if we consider formulas up-to the equivalence relation $\feq$.
Otherwise, in order to properly define the linear negation,
we should fix a permutation $\sigma_\gP$ for each graphical connective $\gP\in\primecon$
in such a way
either $\sigma_P$ is an involution (in case $\gG_\gP\sim \cneg{\left(\gG_\gP\right)}$),
or $\sigma_P\sigma_Q$ is the identity (in case $\gG_\gP\not\sim\cneg{\left(\gG_\gP\right)}\sim\gG_\gQ$ for a $\gQ\in\primecon\setminus\set\gP$).

The linear implication $\fA\limp\fB$ is defined as $\cneg\fA\lpar\fB$,
the logical equivalence $\fA\limpeq\fB$ is defined as $(\fA\limp\fB)\ltens(\fB\limp\fA)$.

As explained in [5] (Section 9), the graphical connectives we discuss in this paper are multiplicative connectives (in the sense of [22, 32, 48, 6]) but they are not the same as the connectives-as-partitions discussed in these works.
In fact,
there is a unique $4$-ary graphical connective $\Pfour$ has symmetry group $\set{\idperm,(1,4)(2,3)}$,
as shown in
[48, 6],
there is a unique pair of dual “primitive” $4$-ary multiplicative connectives-as-partitions $\mathsf G_4$ and $\cneg{\mathsf G_4}$,
$\Sym{\Pfour}\subsetneq\Sym{\mathsf G_4}=\Sym{\cneg{\mathsf G_4}}$.

The following result is consequence of <Ref>.

Let $\fA$ and $\fB$ be formulas.
If $\fA\feq\fB$, then $\gof\fA\greq\gof\fB$.
Moreover, if $\fA$ and $\fB$ are unit-free,
then $\fA\feq\fB$ iff $\gof\fA\greq\gof\fB$.

Note that the the stronger result does not hold in presence of units.
For an example consider the formulas $\funit\ltens\funit$ and $\funit\lpar\funit$.

§ SEQUENT CALCULI OVER OPERATING ON GRAPHS-AS-FORMULAS

We assume the reader to be familiar with the definition of sequent calculus derivations as trees of sequents (see, e.g., [61]) but we recall here some definitions.

We define a sequent is a set of occurrences of formulas.

A sequent system $\Sys$ is a set of sequent rules as the ones in <Ref>.
In a sequent rule $\rho$, we say that a formula is active if
it occurs in one of its premises
but not in its conclusion
, and
principal if it occurs in its conclusion but in none of its premises.

A proof of a sequent $\Gamma$ is a derivation with no open premises, denoted $\vlderivation{\vlpr{\pi}{\Sys}{\Gamma}}$.

We denote by
an (open) derivation of $\Gamma$ from $\Gamma'$,
that is,
is a proof tree having exactly one open premise $\Gamma'$.

A rule is admissible in $\Sys$
if there is a derivation of the conclusion of the rule
whenever all premises of the rule are derivable.
A rule is derivable in $\Sys$,
if there is a derivation in $\Sys$ from the premises to the conclusion of the rule.

In this paper we use the same notation to denote a sequent system $\Sys$

the set of formulas admitting a proof in $\Sys$.

max width=$
\begin{array}{c}
\vlinf{\axrule}{}{\vdash a , \cneg a}{}
\qquad
\vlinf{\lparr}{}{\vdash\Gamma, \fA\lpar \fB}{\vdash \Gamma ,\fA,\fB}
\qquad
\vliinf{\ltensr}{}{\vdash \Gamma, \fA\ltens \fB, \Delta}{\vdash \Gamma, \fA}{\vdash \fB,\Delta}
\\\\
\vliiinf{\dconr[\con]}{
\text{\scriptsize$\begin{cases}\sigma\in\Sym{\con}\\\tau\in\Sym{\cneg\con}\end{cases}$}
\vdash\Gamma_1, \ldots, \Gamma_n, \con\connn{\fA_1, \ldots, \fA_n}, \ncon\connn{\fB_{1}, \ldots \fB_{n}}
\vdash\Gamma_1, \fA_{\sigma(1)}, \fB_{\tau(1)}
\qquad\cdots\qquad
\vdash\Gamma_n, \fA_{\sigma(n)},\fB_{\tau(n)}
\\\\\hline\\
%			%
%			\vlinf{\urule}{}{\vdash \funit , \funit}{}
\qquad
\vliinf{\mixr}{}{\vdash\Gamma_1, \Gamma_2}{\vdash\Gamma_1}{\vdash\Gamma_2}
\qquad
\vliinf{\wdtr}{
\vdash \Gamma, \Delta,
\con\connn{\fA_1,\ldots, \fA_n}
\vdash \Gamma, \fA_k
\vdash \Delta,\con\connn{\fA_1,\ldots, \fA_{k-1},\funit,\fA_{k+1},\ldots,\fA_n}
\\\\
\vlinf{\unitor}{
\dagger
\vdash \Gamma,
%			\underbrace{
\con\connn{\fA_1,\ldots, \fA_k,\funit,\fA_{k+1},\ldots,\fA_n}
%			}_\fA
\vdash \Gamma,\fC\connn{\fA_{\sigma(1)},\ldots, \fA_{\sigma(n)}}
\\\\
\dagger
\coloneqq
\sigma\in\Sym{\fC}
\quand
\gof{\con\connn{\fA_1,\ldots, \fA_k,\funit,\fA_{k+1},\ldots,\fA_n}}
\gof{\fC\connn{\fA_{\sigma(1)},\ldots, \fA_{\sigma(n)}}}
\neq
\unit
%			\\\\\hline\hline\\
%			%
%			%
%			\vlinf{\AXrule}{}{\vdash \fA , \nfA}{}
%			%
%			\qquad
%			%
%			\vliinf{\cutr}{}{\vdash\Gamma_1, \Gamma_2}{\vdash\Gamma_1,\fA}{\vdash\Gamma_2, \cneg \fA}
%			%
%			\qquad
%			%
%			\vliinf{\ctr}{
%				\text{\scriptsize{$\fcC\conso \neq\chole$}}
%			}{\vdash \Gamma_1, \Gamma_2, \fcC\cons \fA}{\vdash\Gamma_1, \fA} {\vdash \Gamma_2, \fcC\consfu}
%			%
%			\qquad
%			%
%			\vlinf{\cpr}{
%				\text{\scriptsize{$\fcC\conso \neq\chole$}}
%			}{\vdash\Gamma, \fcC\consfu, \fA}{\vdash\Gamma, \fcC\cons \fA}
%			%
%			\\\\
%			%
%			\vliiinf{\dconr[\fC]}{
%				\text{\scriptsize $\begin{cases}\sizeof\fC>1\\\sigma\in\Sym{\fC}\\\tau\in\Sym{\nfC}\end{cases}$}
%			}{
%				\vdash\Gamma_1, \ldots, \Gamma_n, \fC\connn{\fA_1, \ldots, \fA_n}, \nfC\connn{\fB_{1}, \ldots \fB_{n}}
%			}{
%				\vdash\Gamma_1, \fA_{\sigma(1)}, \fB_{\tau(1)}
%			}{
%				\qquad\cdots\qquad
%			}{
%				\vdash\Gamma_n, \fA_{\sigma(n)},\fB_{\tau(n)}
%			}
%			%
%			\\\\
%			%
%			\vliinf{\sur}{
%				\text{\scriptsize$\begin{cases}
%						n>1
%						\\
%						\gof{\con\connn{\fA_1,\ldots, \fA_{k-1},\funit,\fA_{k+1},\ldots,\fA_n}}
%						=
%						\gof{\fC\connn{\fA_{\sigma(1)},\ldots, \fA_{\sigma(n-1)}}}
%						\\
%						\sigma\in\Sym{\fC}
%					\end{cases}$}
%			}{
%				\vdash \Gamma,
%				\con\connn{\fA_1,\ldots,\fA_n}
%			}{
%				\vdash \Gamma,\fA_k
%			}{
%				\vdash \Delta,\fC\connn{\fA_{\sigma(1)},\ldots, \fA_{\sigma(n-1)}}
%			}
\end{array}
Linear sequent calculus rules for $\PML$ and $\PMLx$.

We define the following sequent systems using the rules in <Ref>.

\begin{equation}\label{eq:linSyss}
\begin{array}{ll@{\;=\;}l}
\mbox{\defn{Multiplicative Graphical Logic}}\colon\;
\PML
\Set{\axrule,\lparr,\ltens,\dconr[\gP] \mid  \gP\in\primecon}
\\
\mbox{\defn{Multiplicative Graphical Logic with mix}}\colon\;
\PMLx
\PML\cup\Set{\mixr,\wdtr,\unitor}
\\
%			&
%			\PMLe
%			&
%			\Set{\axrule,\mlparr,\mixr,\mltensr,\dconr,\sur \mid\con\in \conset}
%			\mbox{\defn{Classical Prime  Logic}}
%			&
%			\PLK
%			&
%			\PML\cup\set{\wrule,\crule}
\end{array}
\end{equation}

[Rules Exegesis]
The rules axiom ($\axrule$), par ($\lparr$), tensor ($\ltensr$), cut ($\cutr$), and mix ($\mixr$)
are the standard as in multiplicative linear logic with mix.
Note that $\axrule$ is restricted to atomic formulas.

The dual connectives rule ($\dconr$) handles a pair of dual connectives at the same time.
Rules handling multiple operators at the same time are not a novelty in structural proof theory:
in focused proof systems (see, e.g.[10, 51, 50])
rules can handle multiple connectives of a same formula,
in modal logic and linear logic (see, e.g.,  [31, 13, 15, 45])
is quite standard to have rules handling modalities occurring in different formulas of a same sequent.

To get an intuition of this rule,
consider the right-conjunction rule ($\land_R$) used in two-sided sequent calculi for classical logic shown below on the left.
The interpretation of this rule is that if the left premise and the right premise are derivable, then the conclusion is.
Note that, even if the rule does not introduce a conjunction on the lefthand-side of the $\vdash$,
the interpretation of the conclusion sequent is the same of the interpretation of the sequent in which $\fA_1$ and $\fA_2$ are in conjunction
because the standard interpretation of a two-sides sequent $\Gamma \vdash \Delta$ is defined as
$\left(\bigwedge_{\fA\in\Gamma}\cneg\fA \right)\lor \left(\bigvee_{\fB\in\Delta}\fB\right)$.

\begin{equation*}
\adjustbox{max width=\textwidth}{$
\begin{array}{c|c}
\vliiinf{\land_R}{}{
\Gamma_1,\Gamma_2, \fA_1, \fA_2
\vdash
\fB_1\land\fB_2 , \Delta_1,\Delta_2
\vmod1{\Gamma_1, \fA_1\vdash\fB_1,\Delta_1}
\vmod2{\Gamma_2, \fA_2\vdash\fB_2,\Delta_2}
%					\Gedges{mod1/mod2}
\vlinf{}{}{
\Gamma_1,\Gamma_2,\Gamma_3, \Gamma_4, \con[\Pfour]\connn{\fA_1,\fA_2,\fA_3,\fA_4}
\vdash
\con[\Pfour]\connn{\fB_1,\fB_2,\fB_3,\fB_4},
\Delta_1,\Delta_2,\Delta_3,\Delta_4
\Pfour\Connn{
\vmod1{ \Gamma_1, \fA_1\vdash\fB_1,\Delta_1}
\;,\;
%					\qquad
\vmod2{ \Gamma_2, \fA_2\vdash\fB_2,\Delta_2}
%					\qquad
\;,\;
\vmod3{ \Gamma_3, \fA_3\vdash\fB_3,\Delta_3}
\;,\;
%					\qquad
\vmod4{ \Gamma_4, \fA_4\vdash\fB_4,\Delta_4}
%					\Gedges{mod1/mod2,mod2/mod3,mod3/mod4}
\end{array}
\end{equation*}

In a two-sided setting the rule $\dconr$ could have been reformulated by introducing the same connective in both sides.
Intuitively, such a rule would internalize in the logic a meta-connective establishing a relation between the premises of the rule,
as intuitively shown above on the right for the connective $\Pfour$.

The names of the rules
unitor ($\unitor$)
weak-distributivity ($\wdtr$)
are inspired by
the literature of monoidal categories [47]
weakly distributive categories [59, 20, 19].

The rule $\unitor$ internalize the fact that the unit $\funit$ is the neutral element for all connectives
(its side condition prevents the creation of non-pure formulas).

Under the assumption of the existence of a $\funit$ which is the unit of both $\ltens$ and $\lpar$,
the rule $\wdtr$ generalizes the weak-distribution law (shown below on the left) of the $\ltens$ over the $\lpar$ to the weak-distributivity of $\ltens$ over any connective (see below on the top-right)

\begin{equation}\label{eq:WD}
\adjustbox{max width=.92\textwidth}{$
\begin{array}{c|c}
\fA\ltens(\fB\lpar\fC)\longrightarrow(\fA\ltens\fB)\lpar \fC
\begin{array}{c@{\;\longrightarrow\;}c}
\fC\ltens\con\connn{\fA_1,\ldots, \fA_{k}, \fB,\fA_{k+1},\ldots, \fA_n}
\con\connn{\fA_1,\ldots, \fA_k, \fB\ltens \fC,\fA_{k+1},\ldots, \fA_n}
\\
\con\connn{\fA_1,\ldots, \fA_k, \fB\lpar\fC,\fA_{k+1},\ldots, \fA_n}
\con\connn{\fA_1,\ldots, \fA_k, \fB,\fA_{k+1},\ldots, \fA_n}\lpar \fC
\end{array}
\end{array}
\end{equation}

Note that an additional law is required to formalize the weak-distributivity law of all connectives over $\lpar$ (see above on the bottom-right). This law corresponds to the rule $\wdpr$ in <Ref>.

Unless strictly needed for sake of clarity,
we omit to the permutations over the indices of the subformulas in rules.

§.§ Properties of the systems $\PML$ and $\PMLx$

max width=$
\begin{array}{c}
\vlinf{\AXrule}{\text{\scriptsize $\fA$ pure}}{\vdash \fA , \nfA}{}
\qquad
\vliinf{\cutr}{}{\vdash\Gamma_1, \Gamma_2}{\vdash\Gamma_1,\fA}{\vdash\Gamma_2, \cneg \fA}
\qquad
\vlinf{\wdpr}{}{\vdash\Gamma, \con\connn{\funit,\fB_1,\ldots, \fB_n}, \fA}{\vdash\Gamma, \con\connn{\fA,\fB_1,\ldots, \fB_n}}
\\\\
\vliinf{\deepr}{\text{\scriptsize$\gof{\fcC\consfu}=\gof\fB$}}{
\vdash \Gamma, \Delta,
\fcC\cons{\fA}
\vdash \Gamma, \fA
\vdash \Delta,\fB
\qquad
\vliiinf{\dconr[\fC]}{
\text{\scriptsize $\begin{cases}\sigma\in\Sym{\fC}\\\tau\in\Sym{\nfC}\end{cases}$}
\vdash\Gamma_1, \ldots, \Gamma_n, \fC\connn{\fA_1, \ldots, \fA_n}, \nfC\connn{\fB_{1}, \ldots \fB_{n}}
\vdash\Gamma_1, \fA_{\sigma(1)}, \fB_{\tau(1)}
\qquad\cdots\qquad
\vdash\Gamma_n, \fA_{\sigma(n)},\fB_{\tau(n)}
\end{array}
Admissible rules in $\PMLx$.

We start by observing that these systems are initial coherent [11, 50], that is, we can derive the implication $\fA\limp\fA$ for any formula $\fA$ only using atomic axioms.

To prove this result we observe that the generalized version of $\dconr$ (that is, the rule $\dconr[\fC]$) is derivable
by induction on the structure of $\fC$ using the rule $\dconr$.
Therefore, we can prove that the generalized non-atomic axiom rule ($\AXrule$) is derivable, and that both $\PML$ and $\PMLx$ are initial coherent

Let $\fC$ be a pure formula.
Then rule $\dconr[\fC]$ is derivable.

By induction on the structure of $\fC$:

* if $\fA=a$ is a literal, then $\AXrule$ is an instance of $\axrule$;

* if $\fA=\con\connn{\fB_1,\ldots, \fB_k,\funit,\fB_{k+1},\ldots, \fB_n}$, then apply twice $\unitor$ to the sequent $\vdash \fA ,\nfA$ to obtain the sequent of pure formulas  $\vdash \con[\fC]\connn{\fB_1,\ldots, \fB_n},\con[\nfC]\connn{\nfB_1,\ldots, \nfB_n}$.
We conclude by inductive hypothesis;

* if $\fA=\con\connn{\fB_1,\ldots, \fB_n}$ and $\fB_i\neq\funit$ for all $i\in\intset1n$,
then apply the rule $\dconr$ to obtain sequents of pure formulas the form $\fB_i,\nfB_i$ for all $i\in\intset1{\aryof{\con}}$.
We conclude by inductive hypothesis.

The rule $\AXrule$ is derivable in $\PML$ and in $\PMLx$.

The systems $\PML$ and $\PMLx$ are initial coherent (with respect to pure formulas).

We then prove the admissibility of $\cutr$ via cut-elimination by providing a cut-elimination procedure.

Let $\XS\in\set{\PML,\PMLx}$.
The rule $\cutr$ is admissible in $\XS$.

We define the size of a formula as sum of the number of $\funit$, connectives and twice the number of literals in it.
The size of a derivation is the sum of the sizes of the active formulas in all $\cutr$-rules.

The result follows by the fact that each cut-elimination step from <Ref> reduces the size of a derivation.

Note that in order to ensure that both active formulas of a $\cutr$ are principal with respect to the rule immediately above it we also need to consider the commutative cut-elimination steps from <Ref>.
The treatment of these rule, as well as the definition of a size taking into account them, is not covered in the detail here because it is standard in the literature (see, e.g., [61]).

Let $\XS\in\set{\PML,\PMLx}$.
If $\proves[\XS]\fA\limp \fB$ and $\proves[\XS]\fB\limp \fC$, then $\proves[\XS]\fA\limp \fC$.

max width=$\begin{array}{c}
%vs axiom
\vlderivation{
\vliin{\cutr}{}{\vdash a,\Gamma}{
\vlin{\axrule}{}{\vdash a,\cneg a}{\vlhy{}}
\vlhy{\vdash a, \Gamma}
\;\rightsquigarrow\;
\vdash \cneg a,\Gamma
\qquad
% tens vs par
\vlderivation{
\vliin{\cutr}{}{
\vdash\Gamma,\Delta,\Sigma
\vliin{\ltensr}{}{
\vdash\Gamma, \Delta, \fA\ltens\fB
\vlhy{\vdash\Gamma,\fA}
\vlhy{\vdash\Delta,\fB}
\vlin{\lparr}{}{
\vdash \Sigma, \nfA \lpar \nfB
\vlhy{\vdash\Sigma, \nfA\lpar\nfB}
\;\rightsquigarrow\;
\vlderivation{
\vliin{\cutr}{}{
\vdash\Gamma,\Delta,\Sigma
\vlhy{\vdash\Gamma,\fA}
\vliin{\cutr}{}{
\vdash \Delta,\Sigma, \nfA
\vlhy{\vdash\Delta,\fB}
\vlhy{\vdash\Sigma, \nfA,\nfB}
%			\vlderivation{
%				\vliin{\cutr}{}{
%					\vdash\Gamma_1,\ldots, \Gamma_n,\Delta
%				}{
%					\vliiin{\mltensr}{}{\vdash\Gamma_1,\ldots, \Gamma_n, \mltens\connn{\fA_1,\ldots, \fA_n} }{\vlhy{\vdash\Gamma_1,\fA_1}}{\vlhy{\cdots}}{\vlhy{\vdash\Gamma_n,\fA_n}}
%				}{
%					\vlin{\mlparr}{}{\vdash\Delta, \mlpar\connn{\nfA_1,\ldots, \nfA_n}}{\vlhy{\vdash\Delta, \nfA_1,\ldots, \nfA_n}}
%				}
%			}
%			%
%			\;\rightsquigarrow\;
%			%
%			\vlderivation{
%				\vliin{\cutr}{}{
%					\vdash\Gamma_1,\ldots, \Gamma_n,\Delta
%				}{
%					\vlhy{\vdash\Gamma_1,\fA_1}
%				}{
%					\vliin{\cutr}{}{
%						\reflectbox{$\ddots$}
%					}{
%						\vlhy{\vdash\Gamma_{n},\fA_n}
%					}{
%						\vlhy{\vdash\Delta, \nfA_1,\ldots, \nfA_n}
%					}
%				}
%			}
\\\\\hline\\
%dconr vs drule
\vlderivation{
\vliin{\cutr}{}{
\vdash\Gamma_1,\ldots, \Gamma_n, \Delta_1, \ldots, \Delta_n,\con\connn{\fA_1, \ldots, \fA_n},\ncon\connn{\fC_1,\ldots, \fC_n}
\vliiin{\dconr}{}{
\vdash\Gamma_1,\ldots, \Gamma_n, \con\connn{\fA_1, \ldots, \fA_n},\ncon\connn{\fB_1, \ldots, \fB_n}
\vliiin{\dconr}{}{
\vdash\Delta_1,\ldots, \Delta_n, \con\connn{\nfB_1, \ldots, \nfB_n},\ncon\connn{\fC_1,\ldots, \fC_n}
%				\;\rightsquigarrow\;
\\\downsquigarrow\\
\vlderivation{
\vliiin{\dconr}{}{
\vdash\Gamma_1,\ldots, \Gamma_n, \Delta_1, \ldots, \Delta_n,\ncon\connn{\fB_1, \ldots, \fB_n},\con\connn{\fC_1,\ldots, \fC_n}
\vliin{\cutr}{}{\vdash\Gamma_1,\Delta_1,\fA_1,\fC_1}{\vlhy{\vdash\Gamma_1,\fA_1,\fB_1}}{\vlhy{\vdash\Delta_1,\nfB_1,\fC_1}}
\vlhy{\quad\cdots\quad}
\vliin{\cutr}{}{\vdash\Gamma_n,\fA_n,\fC_n}{\vlhy{\vdash\Gamma_n,\fA_n,\fB_n}}{\vlhy{\vdash\Delta_n,\nfB_n,\fC_n}}
\end{array}$
Cut-elimination steps for $\PML$.

max width=$\begin{array}{c}
%unit vs unit
%		\vlderivation{
%			\vliin{\cutr}{}{\vdash \funit,\funit}{
%				\vlin{\urule}{}{\vdash \funit, \funit}{\vlhy{}}
%			}{
%				\vlhy{\vdash \funit, \Gamma}
%			}
%		}
%		%
%		\;\rightsquigarrow\;
%		%
%		\vdash \funit,\Gamma
%		%
%		\\\\\hline\\
% good unitor vs unitor
\vlderivation{
\vliin{\cutr}{}{
\vdash\Gamma,\Delta
\vlin{\unitor}{}{
\vdash\Gamma, \fP\connn{\funit,\fA_2, \ldots, \fA_n}
\vlhy{\vdash\Gamma, \fC\connn{\fA_2,\ldots, \fA_n}}
\vlin{\unitor}{}{
\vdash \Delta, \nfP\connn{\funit,\nfA_2, \ldots, \nfA_n}
\vlhy{\vdash\Delta, \nfC\connn{\nfA_2,\ldots, \nfA_n}}
\;\rightsquigarrow\;
\vlderivation{
\vliin{\cutr}{}{
\vdash\Gamma,\Delta
\vlhy{\vdash\Gamma, \fC\connn{\fA_2,\ldots, \fA_n}}
\vlhy{\vdash\Delta, \nfC\connn{\nfA_2,\ldots, \nfA_n}}
\\\\\hline\\
% good wd vs wd
\vlderivation{
\vliin{\cutr}{}{
\vdash\Gamma_1,\Gamma_2,\Delta_1,\Delta_2
\vliin{\wdtr}{}{
\vdash\Gamma_1,\Gamma_2, \fP\connn{\fA_1, \ldots, \fA_n}
\vlhy{\vdash\Gamma_1,\fA_1}
\vlhy{\vdash\Gamma_2, \fP\connn{\funit,\fA_2,\ldots, \fA_n}}
\vliin{\wdtr}{}{
\vdash\Delta, \nfP\connn{\nfA_1, \ldots, \nfA_n}
\vlhy{\vdash\Delta_1,\nfA_1}
\vlhy{\vdash\Delta_2, \nfP\connn{\funit,\nfA_2,\ldots, \nfA_n}}
\\\downsquigarrow\\\\
\vlderivation{
\vliin{\mixr}{}{
\vdash\Gamma_1,\Gamma_2,\Delta_1,\Delta_2
\vliin{\cutr}{}{
\vdash\Gamma_1,\Delta_1
\vlhy{\vdash\Gamma_1,\fA_1}
\vlhy{\vdash\Delta_1,\nfA_1}
\vliin{\cutr}{}{
\vdash\Gamma_2,\Delta_2
\vlhy{\vdash, \Gamma_2,\fP\connn{\funit,\fA_2,\dots \fA_n}}
\vlhy{\vdash\Delta_2, \nfP\connn{\funit,\nfA_2,\dots \nfA_n}}
%		\\\\\hline\\
%		% dcon vs unitor
%		\vlderivation{
%			\vliin{\cutr}{}{
%				\vdash\Gamma_1,\ldots, \Gamma_n, \Delta_1,\Delta_2,\fP\connn{\fA_1, \ldots, \fA_n}
%			}{
%				\vliiin{\dconr}{}{
%					\vdash\Gamma_1,\ldots, \Gamma_n, \fP\connn{\funit,\fA_2, \ldots, \fA_n},\nfP\connn{\funit,\fB_2, \ldots, \fB_n}
%				}{
%					\vlin{\urule}{}{\vdash \funit, \funit}{\vlhy{}}
%				}{
%					\vlhy{\vdash\Gamma_2,\fA_2,\fB_2\qquad\cdots\qquad}
%				}{
%					\vlhy{\vdash\Gamma_n,\fA_n,\fB_n}
%				}
%			}{
%				\vlin{\unitor}{}{
%					\vdash \Delta, \fP\connn{\funit,\nfB_2, \ldots, \nfB_n}
%				}{
%					\vlhy{\vdash \Delta, \fC\connn{\nfB_2,\ldots, \nfB_n}}
%				}
%			}
%		}
%		%
%		\\\downsquigarrow\\\\
%		%
%		\vlderivation{
%			\vliin{\wdtr}{}{
%				\vdash\Gamma_1,\ldots, \Gamma_n, \Delta_1,\Delta_2,\fP\connn{\fA_1, \ldots, \fA_n}
%			}{
%				\vliin{\cutr}{}{
%					\vdash \Gamma_1, \Delta_1, \fA_1
%				}{
%					\vlhy{\vdash \Gamma_1, \fA_1,\fB_1}
%				}{
%					\vlhy{\vdash \Delta_1, \nfB_1}
%				}
%			}{
%				\vlin{\unitor}{}{
%					\vdash \Gamma_2,\ldots, \Gamma_n,\Delta_2, \fP\connn{\funit,\fA_2, \ldots, \fA_n}
%				}{
%					\vliin{\cutr}{}{
%						\vdash \Gamma_2,\ldots, \Gamma_n,\Delta_2, \fC\connn{\fA_2, \ldots, \fA_n}
%					}{
%						\vliiin{\dconr[\fC]}{}{
%							\vdash\Gamma_2,\ldots, \Gamma_n, \fC\connn{\fA_1, \ldots, \fA_n},\nfC\connn{\fB_1, \ldots, \fB_n}
%						}{
%							\vlhy{\vdash\Gamma_2,\fA_2,\fB_2}
%						}{
%							\vlhy{\qquad\cdots\qquad}
%						}{
%							\vlhy{\vdash\Gamma_n,\fA_n,\fB_n}
%						}
%					}{
%						\vlhy{\vdash \Delta_2, \fC\connn{\nfB_2,\ldots, \nfB_n}}
%					}
%				}
%			}
%		}
\\\\\hline\\
% dcon vs wd
\vlderivation{
\vliin{\cutr}{}{
\vdash\Gamma_1,\ldots, \Gamma_n, \Delta,\Sigma,\fP\connn{\fA_1, \ldots, \fA_n}
\vliiin{\dconr}{}{
\vdash\Gamma_1,\ldots, \Gamma_n, \fP\connn{\fA_1, \ldots, \fA_n},\nfP\connn{\fB_1, \ldots, \fB_n}
\vlhy{\vdash\Gamma_1,\fA_1,\fB_1}
\vlhy{\qquad\cdots\qquad}
\vlhy{\vdash\Gamma_n,\fA_n,\fB_n}
\vliin{\wdtr}{}{
\vdash \Delta,\Sigma, \fP\connn{\nfB_1, \ldots, \nfB_n}
\vlhy{\vdash \Delta,\nfB_1}
\vlhy{\vdash \Sigma, \fP\connn{\funit,\nfB_2,\ldots, \nfB_n}}
\\\downsquigarrow\\\\
\vlderivation{
\vliin{\wdtr}{}{
\vdash\Gamma_1,\ldots, \Gamma_n, \Delta,\Sigma,\fP\connn{\fA_1, \ldots, \fA_n}
\vliin{\cutr}{}{
\vdash \Gamma_1, \Delta, \fA_1
\vlhy{\vdash \Gamma_1, \fA_1,\fB_1}
\vlhy{\vdash \Delta, \nfB_1}
\vliin{\cutr}{}{
\vdash \Gamma_2,\ldots, \Gamma_n,\Sigma, \fP\connn{\funit,\fA_2, \ldots, \fA_n}
\vlin{2\times \unitor}{}{
\vdash\Gamma_2,\ldots, \Gamma_n,
\fP\connn{\funit,\fA_1, \ldots, \fA_n},
\nfP\connn{\funit,\fB_1, \ldots, \fB_n}
\vliin{\dconr[\fC]}{}{
\vdash\Gamma_2,\ldots, \Gamma_n,
\con[\fC]\connn{\fA_1, \ldots, \fA_n},
\ncon[\fC]\connn{\fB_1, \ldots, \fB_n}
\vlhy{\vdash\Gamma_2,\fA_2,\fB_2\qquad\cdots\qquad}
\vlhy{\vdash\Gamma_n,\fA_n,\fB_n}
\vlhy{\vdash \Sigma, \fP\connn{\funit,\nfB_2,\ldots, \nfB_n}}
\end{array}$

Additional cut-elimination steps in $\GMLx$.

max width=$\begin{array}{c}
\vlderivation{
\vliin{\cutr}{}{\vdash\Gamma_1, \Gamma_2,\Delta}{
\vlin{\rho}{}{\vdash\Gamma_1,\Delta, \fA}{
\vlhy{\vdash\Gamma_1,\Delta',\fA}
\vlhy{\vdash\nfA,\Gamma_2}
\quad\rightsquigarrow\quad
\vlderivation{
\vlin{\rho}{}{\vdash\Gamma_1, \Gamma_2,\Delta'}{
\vliin{\cutr}{}{\vdash\Gamma_1,\Gamma_2,\Delta}{
\vlhy{\vdash\Gamma_1,\Delta',\fA}
\vlhy{\vdash\nfA,\Gamma_2}
\\\\
\vlderivation{
\vliin{\cutr}{}{
\vdash\Gamma_1,\ldots, \Gamma_{n+1},\Delta
\vliiin{\rho}{}{
\vdash\Gamma_1,\ldots, \Gamma_n, \Delta,\fA
\vlhy{\vdash\Gamma_1, \Delta_1'}
\vlhy{\vdash\Gamma_n,\Delta_n',\fA}
\vlhy{\vdash\nfA,\Gamma_{n+1}}
\quad\rightsquigarrow\quad
\vlderivation{
\vliiiin{\rho}{}{
\vdash\Gamma_1,\ldots,\Gamma_{n+1},\Delta
\vlhy{\vdash\Gamma_1, \Delta_1'}
\vlhy{\vdash\Gamma_{n-1},\Delta_{n-1}'}
\vliin{\cutr}{}{
\vdash\Gamma_n,\Gamma_{n+1},\Delta_n'
\vlhy{\vdash\Gamma_n,\Delta_n',\fA}
\vlhy{\vdash\Gamma_{n+1},\nfA}
\\\\
\vlderivation{
\vlin{\unitor}{}{
\vdash
\Gamma
\fP\connn{\fA_1,\ldots, \fA_{i-1},\funit,\fA_{i+1},\ldots,\fA_{j-1},\funit,\fA_{j+1},\ldots,  \fA_n}
\vlin{\unitor}{}{
\vdash
\Gamma,
\fcon{\gP}\connn{\fA_1,\ldots, \fA_{i-1},\funit,\fA_{i+1},\ldots,\fA_{j-1},\fA_{j+1},\ldots,  \fA_n}
\vlhy{
\vdash
\Gamma,
\fC\connn{\fA_1,\ldots, \fA_{i-1},\fA_{i+1},\ldots,\fA_{j-1},\fA_{j+1},\ldots,  \fA_n}}
\;\rightsquigarrow\;
\vlderivation{
\vlin{\unitor}{}{
\vdash
\Gamma,
\fP\connn{\fA_1,\ldots, \fA_{i-1},\funit,\fA_{i+1},\ldots,\fA_{j-1},\funit,\fA_{j+1},\ldots,  \fA_n}
\vlin{\unitor}{}{
\vdash
\Gamma,
\fcon{\gP'}\connn{\fA_1,\ldots, \fA_{i-1},\fA_{i+1},\ldots,\fA_{j-1},\funit,\fA_{j+1},\ldots,  \fA_n}
\vlhy{
\vdash
\Gamma,
\fC\connn{\fA_1,\ldots, \fA_{i-1},\fA_{i+1},\ldots,\fA_{j-1},\fA_{j+1},\ldots,  \fA_n}}
\end{array}$

Commutative cut-elimination steps.

The admissibility of the $\cutr$-rule implies analyticity of $\PML$ via the standard sub-formula property, that is, all (occurrences of) formulas occurring in the premises of a rule are subformulas of the ones in the conclusion.

Let $\Gamma$ be a sequent.
If $\proves[\PML]\Gamma$, then there is a proof of $\Gamma$ in $\PML$ only containing occurrences of sub-formulas of formulas $\Gamma$.

However, the same result does not hold for $\PMLx$ because of the rule $\unitor$.
In fact, the presence of more-than-binary connectives and their units (in this case, a unique unit $\funit$) implies,
as observed in the previous works on graphical logic [4, 5, 2],
the possibility of having sub-connectives, that is, connectives with smaller arity behaving as if certain entries of the connective are fixed to be units.

Let $\gP$ and $\gQ$ be prime graphs.
$\gP\connn{\funits, v_{i_1},\funits, v_{i_k},\funits}\isym\gQ\connn{v_1,\dots, v_n}$
for single-vertex graphs $v_1, \ldots,v_n$
for some distinct $i_1,\ldots,i_k\in\intset1n$,

then we may write
$\con[\gP\restr{i_1,\ldots, i_k}]=\con[\gQ]$
and we say that
the connective $\con[\gQ]$ is a sub-connective of if $\con[\gP]$.

A  of a formula

is a formula of the form
$\con[\gP'\restr{i_1,\ldots, i_k}]\connn{\fB'_{i_1},\ldots,\fB'_{i_k}}$
$\fB'_{i_j}$ a of $\fB_{i_j}$ for all $i_j\in\intset{i_1}{i_k}$.

Let $\Gamma$ be a sequent.
If $\proves[\PMLx]\Gamma$ then there is a proof of $\Gamma$ in $\PMLx$ only containing occurrences of of formulas in $\Gamma$.

The logic $\PML$ is a conservative extension of $\MLL$.
The logic $\PMLx$ is a conservative extension of $\MLLx$.

For $\PML$ it is consequence of the subformula property.
For $\PMLx$ it suffices to remark that $\lpar$ and $\ltens$ have no sub-connectives, therefore are simply sub-formulas.

For both $\PML$ and $\PMLx$ we have the following result which takes the name of splitting in the deep inference literature (see, e.g, [8, 35, 36]).
This result states that is always possible, during proof search, to apply a rule removing a connective after having applied certain rules in the context.
Note that in the linear logic literature, the splitting lemma is usually formulated as a special case of the lemma here, where a $\ltens$ is removed without requiring the application of rules to the context.

$\Gamma, \con\connn{\fA_1, \ldots, \fA_n}$ be a sequent
If $\proves[\XS]\Gamma,\con\connn{\fA_1, \ldots, \fA_n} $,
then there is

a derivation of the following shape

\begin{equation*}
\vlderivation{
\vlde{\pi_0}{}{
\vdash \Gamma,\con\connn{\fA_1, \ldots,\fA_{k-1},\funit,\fA_{k+1}, \fA_n}
\vlin{\unitor}{}{
\vdash \Gamma',\con\connn{\fA_1, \ldots,\fA_{k-1},\funit,\fA_{k+1}, \fA_n}
\vlpr{\pi_1}{}{\vdash \Gamma',\fC\connn{\fA_1, \ldots,\fA_{k-1},\fA_{k+1}, \fA_n}}
\qquor
\vlderivation{
\vlde{\pi_0}{}{
\vdash \Gamma,\con\connn{\fA_1, \ldots, \fA_n}
\vdash \Gamma',\con\connn{\fA_1, \ldots, \fA_n}
\vlpr{\pi_1}{}{\vdash \Delta_1,\fA_1}
\vlhy{\cdots}
\vlpr{\pi_n}{}{\vdash \Delta_n,\fA_n}
\mbox{ with  $\rho \in\set{\lparr,\ltensr,\dconr}$}
\end{equation*}

By case analysis of the last rule occurring in a proof $\pi$ of $\Gamma, \con\connn{\fA_1, \ldots, \fA_n}$:

* the last rule cannot be a $\axrule$ since $\con\connn{\fA_1, \ldots, \fA_n}$ contains at least one connective;

* if the last rule is a $\lparr$ or a $\unitor$, then
either this is the desired rule, or we conclude by inductive hypothesis on its premise;

* if the last rule is a $\mixr$, then we conclude by inductive hypothesis on the premise containing the formula $\con\connn{\fA_1, \ldots, \fA_n}$;

* if the last rule is in $\set{\ltensr,\dconr,\wdtr,\unitor}$
then either this is the desired rule or one of the (provable) premises of this rule is of the shape $\Gamma',\con\connn{\fA_1, \ldots, \fA_n}$,
allowing us to conclude by inductive hypothesis.

We conclude this section proving the admissibility of the rule
$\wdpr$ which we use to simplify proofs in the next section.

The rule $\wdpr$ is admissible in $\PMLx$.

In <Ref> we providde a procedure to remove (top-down) all occurrences of $\wdpr$.
Similar to cut-elimination, we use the commutative steps from <Ref>
to ensure that the active formula of the $\wdpr$ we want to remove is principal with respect to the rule immediately above it.

max width = $\begin{array}{c}
\vlderivation{
\vlin{\wdpr}{}{
\vdash \Gamma, \fA,\funit\lpar \fB
\vlin{\lparr}{}{
\vdash \Gamma, \fA\lpar \fB
\vlpr{\pi_1}{}{\vdash \Gamma, \fA, \fB}
\wdprred
\vlderivation{
\vlin{\unitor}{}{
\vdash \Gamma, \fA,\funit\lpar \fB
\vlpr{\pi_1}{}{\vdash \Gamma, \fA,\fB}
\qquad\qquad
\vlderivation{
\vlin{\wdtr}{}{
\vdash \Gamma, \Delta, \fA,\funit\ltens \fB
\vliin{\ltensr}{}{
\vdash \Gamma, \Delta, \fA\ltens \fB
\vlpr{\pi_1}{}{\vdash \Gamma, \fA}
\vlpr{\pi_2}{}{\vdash \Delta, \fB}
\wdprred
\vlderivation{
\vlin{\unitor}{}{
\vdash \Gamma, \Delta, \fA, \funit\ltens\fB
\vliin{\mixr}{}{
\vdash \Gamma, \Delta, \fA, \fB
\vlpr{\pi_1}{}{\vdash \Gamma, \fA}
\vlpr{\pi_2}{}{\vdash \Delta, \fB}
\\\\
\vlderivation{
\vlin{\wdpr}{}{
\vdash \Gamma_1,\ldots, \Gamma_n, \ncon\connn{\fB_1,\ldots, \fB_n}, \con\connn{\funit, \fA_2, \ldots, \fA_n},\fA
\vliiiin{\dconr}{}{
\vdash \Gamma_1,\ldots, \Gamma_n, \ncon\connn{\fB_1,\ldots, \fB_n}, \con\connn{\fA, \fA_2, \ldots, \fA_n}
\vlpr{\pi_1}{}{\vdash \Gamma_1, \fA, \fB_1 }
\vlpr{\pi_2}{}{\vdash \Gamma_2, \fA_2,\fB_2}
\vlpr{\pi_n}{}{\vdash \Gamma_n, \fA_n,\fB_n}
\wdprred
\vlderivation{
\vliin{\wdtr}{}{
\vdash \Gamma_1,\ldots, \Gamma_n,  \ncon\connn{\fB_1,\ldots, \fB_n},
\con\connn{\funit, \fA_2, \ldots, \fA_n},\fA
\vlpr{\pi_1}{}{\vdash \Gamma_1, \fA, \fB_1 }
\vlin{2\times\unitor}{}{
\vdash \Gamma_2,\ldots, \Gamma_n,
\ncon\connn{\funit,\fB_1,\ldots, \fB_n},
\con\connn{\funit, \fA_2, \ldots, \fA_n}
\vliiin{\dconr[\fC]}{}{
\vdash \Gamma_2,\ldots, \Gamma_n,
\nfC\connn{\fB_2,\ldots, \fB_n},
\fC\connn{\fA_2, \ldots, \fA_n}
\vlpr{\pi_2}{}{\vdash \Gamma_2, \fB_2,\fC_2}
\vlpr{\pi_n}{}{\vdash \Gamma_n, \fB_n,\fC_n}
\\\\
\vlderivation{
\vlin{\wdpr}{}{
\vdash \Gamma_1,\Gamma_2, \con\connn{\funit,\fB_2, \ldots, \fB_n},\fA
\vliin{\wdtr}{}{
\vdash \Gamma_1,\Gamma_2, \con\connn{\fA,\fB_2, \ldots, \fB_n}
\vlpr{\pi_1}{}{\vdash \Gamma_1,\fB_{k}}
\vlpr{\pi_2}{}{\vdash \Gamma_2, \con\connn{\fA,\fB_2, \ldots, \fB_{k-1},\funit, \fB_{k+1},\ldots, \fB_n}}
\wdprred
\vlderivation{
\vliin{\wdtr}{}{
\vdash \Gamma, \con\connn{\funit,\fB_2, \ldots, \fB_k,\fB', \fB_{k+1},\ldots, \fB_n},\fA
\vlpr{\pi_1}{}{\vdash \Gamma_1,\fB'}
\vlin{\wdpr}{}{
\vdash \Gamma_2, \con\connn{\funit,\fB_2, \ldots, \fB_{k-1},\funit, \fB_{k+1},\ldots, \fB_n},\fA
\vlpr{\pi_2}{}{\vdash \Gamma_2, \con\connn{\fA,\fB_2, \ldots, \fB_{k-1},\funit, \fB_{k+1},\ldots, \fB_n}}
\\\\
\vlderivation{
\vlin{\wdpr}{}{
\vdash \Gamma, \con\connn{\funit,\fB_2, \ldots, \fB_{n-1},\funit},\fA
\vlin{\unitor}{}{
\vdash \Gamma, \con\connn{\fA,\fB_2, \ldots, \fB_{n-1},\funit}
\vlpr{\pi_1}{}{
\vdash \Gamma, \fC\connn{\fA,\fB_2, \ldots, \fB_{n-1}}
\wdprred
\vlderivation{
\vlin{\unitor}{}{
\vdash \Gamma, \con\connn{\funit,\fB_2, \ldots, \fB_{n-1},\funit},\fA
\vlin{\wdpr}{}{
\vdash \Gamma, \fC\connn{\funit,\fB_2, \ldots, \fB_{n-1}},\fA
\vlpr{\pi_1}{}{
\vdash \Gamma, \fC\connn{\fA,\fB_2, \ldots, \fB_{n-1}}
\end{array}$

Steps to eliminate $\wdpr$ rules.

The rule $\deepr$ is admissible in $\PMLx$.

Since $\fcC\consfu\neq\funit$,
$\fcC\conso=\con\connn{\fcC'\conso,\fB'_1, \ldots,\fB'_n}$.
If $\fcC'\conso=\chole$, then w.l.o.g.,
$\fB=\fC\connn{\fB'_1, \ldots,\fB'_n}$
and we conclude since we have

\vlderivation{
\vliin{\wdpr}{}{
\vdash \Gamma, \Delta, \con\connn{\fA,\fB'_1, \ldots,\fB'_n}
\vlhy{\vdash \Gamma, \fA}
\vlin{\unitor}{}{
\vdash \Delta, \con\connn{\funit,\fB'_1, \ldots,\fB'_n}
\vlhy{\vdash \Delta, \fC\connn{\fB'_1, \ldots,\fB'_n}}

we conclude by inductive hypothesis on the size of $\fcC\conso$
since by <Ref> we can define a derivation of the form

\vlderivation{
\vlde{\pi_0}{}{
\vdash \Gamma,\Delta, \con\connn{\fcC\cons{\fA},\fB_1, \ldots,\fB_{k-1},\funit,\fB_{k+1}\ldots \fB_n}
\vdash \Gamma',\Delta',\con\connn{\fcC\cons{\fA},\fB_1, \ldots,\fB_{k-1},\funit,\fB_{k+1}\ldots \fB_n}
\vlpr{}{\IH}{\vdash \Gamma',\Delta',\fC\connn{\fcC\cons{\fA},\fB_1, \ldots, \fB_n}}
\quor
\vlderivation{
\vlde{\pi_0}{}{
\vdash \Gamma,\Delta, \con\connn{\fcC\cons{\fA},\fB'_1, \ldots,\fB'_n}
\vdash \Gamma',\Delta',\con\connn{\fcC\cons{\fA},\fB'_1, \ldots,\fB'_n}
\vlpr{}{\IH}{\vdash \Gamma', \Delta_0, \fcC\cons{\fA}}
\vlpr{\pi_1}{}{\vdash \Delta_1,\fB'_1}
\vlhy{\cdots}
\vlpr{\pi_n}{}{\vdash \Delta_n,\fB'_n}

with $\rho\in\set{\lparr,\ltensr,\dconr}$.

§.§ Graph Isomorphism as Logical Equivalence

In this sub-section we prove that two formulas $\phi$ and $\psi$ are interpreted by a same graph (i.e., $\gof\phi=\gof\phi$) iff they are logically equivalent (i.e., $\phi\limpeq\psi$).
For this purpose, we show that all equivalence and De Morgan laws from <Ref> can be reformulated as logical equivalences.

We first prove that connectives symmetries are derivable in $\PML$.

The following rules are admissible in $\PML$.

\begin{equation}
\vlidf{\symr}{
\text{\scriptsize$\sigma\in\Sym{\gQ}$}
\vdash\Gamma, \con\connn{\fA_{\sigma(1)}, \ldots, \fA_{\sigma(n)}}
\vdash\Gamma, \con\connn{\fA_1, \ldots, \fA_n}
\qquad
\vlidf{\dsymr}{
\text{\scriptsize$\rho\in\Dsym{\gQ}$}
\vdash\Gamma, \con\connn{\fA_{\rho(1)}, \ldots, \fA_{\rho(n)}}
\vdash\Gamma,\cneg\con\connn{\fA_1, \ldots, \fA_n}
\end{equation}

By <Ref>, it suffices to prove that the following implications are derivable.

\underbrace{
\begin{array}{l}
\con\connn{\fA_1, \ldots, \fA_n }\limp \con\connn{\fA_{\sigma(1)}, \ldots, \fA_{\sigma(n)}}
\\
\con\connn{\fA_{\sigma(1)}, \ldots, \fA_{\sigma(n)}} \limp \con\connn{\fA_1, \ldots, \fA_n}
\end{array}}_{\mbox{ for all }\sigma\in\Sym{\gQ}}
\qquand
\underbrace{
\begin{array}{l}
\con\connn{\fA_1, \ldots, \fA_n }\limp \ncon\connn{\fA_{\rho(1)}, \ldots, \fA_{\rho(n)}}
\\
\ncon\connn{\fA_{\rho(1)}, \ldots, \fA_{\rho(n)}}\limp \con\connn{\fA_1, \ldots, \fA_n}
\end{array}}_{\mbox{ for all }\tau\in\Dsym{\gQ}}

These are easily derivable using an instance of $\dconr$ and $\AXrule$-rules.

The rule $\symr[\lpar]$ is derivable directly because sequents are sets if occurrences of formulas, therefore the order of the occurrences of the formulas in a sequent is not relevant, and we can permute this order before applying the rule $\lpar$.
This because the interpretation of the meta-connective comma we use to separate formulas in a sequent is the same  of $\lpar$.

Similarly, the rule $\symr[\ltens]$ is derivable because in our sequent system, as in standard sequent calculus, the order of the premises of the rules is not relevant.
Said differently, the space between branches in a derivation is a commutative meta-connective which is internalized by the $\ltensr$.

Similarly we can prove that the associativity of $\lpar$ and $\ltens$ is derivable.

The following rules are admissible.

\begin{equation}
\adjustbox{max width = .9\textwidth}{$
\vlidf{\passr}{}{
\vdash\Gamma, \fA_1\lpar(\fA_2\lpar \fA_3)
\vdash\Gamma, (\fA_1\lpar \fA_2)\lpar \fA_3
\qquad
\vlidf{\tassr}{}{
\vdash\Gamma, \fA_1\ltens(\fA_2\ltens \fA_3)
\vdash\Gamma, (\fA_1\ltens \fA_2)\ltens \fA_3
\end{equation}

The result follows by <Ref> after showing that following implications hold:

\fA_1\lpar(\fA_2\lpar \fA_3)
(\fA_1\lpar \fA_2)\lpar \fA_3
(\fA_1\lpar \fA_2)\lpar \fA_3
\fA_1\lpar(\fA_2\lpar \fA_3)
\\
\fA_1\ltens(\fA_2\ltens \fA_3)
(\fA_1\ltens \fA_2)\ltens \fA_3
(\fA_1\ltens \fA_2)\ltens \fA_3
\fA_1\ltens(\fA_2\ltens \fA_3)
\end{array}$$

We can therefore immediately conclude that $\PML$ is sound and complete with respect to graph isomorphism if we consider unit-free formulas.

Let $\fA$ and $\fB$ be unit-free formulas.
Then $\fA\feq\fB$ iff $\proves[\PML]\fA\limpeq \fB$.

By induction on the formulas $\fA$ and $\fB$ using <Ref>.

For a stronger result on general formulas, we need to show that for any two formulas $\fA$ and $\fB$ are interpreted (via $\gof\cdot$) by the same non-empty graph,
both these formulas are equivalent to a unit-free formula $\fC$ representing the modular decomposition of this graph via graphical connectives.

Let $\fA$ and $\fB$ be pure formulas.
Then $\fA\feq\fB$ iff $\proves[\PMLx]\fA\limpeq \fB$.

Given any formula $\fA$, we can define
by induction on the number of units $\funit$ occurring in
a unit-free formula $\fA'$ such that $\fA\limpeq\fA'$.

* if $\fA$ is a literal, then $\fA'=\fA$;

* if $\fA=\con\connn{\fA_1,\ldots, \fA_n}$ and $\fA_i\neq\funit$ for all $i\in\intset1n$, then $\fA'=\con\connn{\fA_1',\ldots, \fA_n'}$.
Otherwise, w.l.o.g., we assume $\fA_i=\funit$ and we let $\fA'=\fC\connn{\fA_2',\ldots, \fA_n'}$ for a compact formula  $\fC$ such that
\gof{\fC\connn{\fA_2,\ldots, \fA_n}}$
and we conclude by inductive hypothesis since we the following derivations:

\hskip-2em
\vlderivation{
\vlin{\lparr}{}{
\vdash
\ncon\connn{\funit,\nfA_2,\ldots,\nfA_n}
\lpar
\fC\connn{\fA'_2,\ldots, \fA'_n}
\vlin{\unitor}{}{
\vdash
\ncon\connn{\funit,\nfA_2,\ldots,\nfA_n}
\fC\connn{\fA'_2,\ldots, \fA'_n}
\vliiin{\dconr[\fC]}{}{
\vdash
\nfC\connn{\nfA_2,\ldots,\nfA_n}
\fC\connn{\fA'_2,\ldots, \fA'_n}
\vlpr{\IH}{}{\vdash \nfA_2,\fA'_2}
\vlpr{\IH}{}{\vdash \nfA_n,\fA'_n}
\quand
\vlderivation{
\vlin{\lparr}{}{
\vdash
\nfC\connn{\fA'_2,\ldots, \cneg{\fA'}_n}
\lpar
\con\connn{\funit,\fA_2,\ldots,\fA_n}
\vlin{\unitor}{}{
\vdash
\nfC\connn{\cneg{\fA'}_2,\ldots, \cneg{\fA'}_n}
\con\connn{\funit,\fA_2,\ldots,\fA_n}
\vliiin{\dconr[\fC]}{}{
\vdash
\nfC\connn{\funit,\cneg{\fA'}_2,\ldots, \cneg{\fA'}_n}
\fC\connn{\funit,\fA_2,\ldots,\fA_n}
\vlpr{\IH}{}{\vdash \cneg{\fA'}_2,\fA_2}
\vlpr{\IH}{}{\vdash \cneg{\fA'}_n,\fA_n}

Therefore we can find unit-free formulas $\fA'$ and $\fB'$ such that
$\fA\limpeq\fA'$ and $\fB\limpeq\fB'$.
Moreover, by definition of $\gof\cdot$ and the rule $\unitor$  we have $\gof\fA'=\gof\fA=\gof\fB=\gof\fB'$.

We conclude by <Ref> and the transitivity of $\limpeq$.

§ SOUNDNESS AND COMPLETENESS OF $\PMLX$ WITH RESPECT TO $\GS$

In this section we prove that set of graphs which are derivable in the graphical logic $\GS$ from [4, 5]
is the same set of graph corresponding to formulas which are provable in $\PMLx$.

In <Ref> we recall the definition of the rules of the deep inference system
The definition of deep inference systems operating on graphs can be found in [5] or in  <Ref>.

At the syntactical level, the system $\GS$ operates on graphs by manipulating their
modular decompositions trees.
Therefore, for any graph occurring in a derivation in $\GS$ we assume a unique formula $\fof\gG$ to be given.

Note that in $\GS$ the authors allow themselves to consider modular decomposition trees in which leaves may be empty graphs, corrisponding to formulas with unit.

max width=$
\begin{array}{c@{\quad}c@{\quad}c@{\quad}c}
\vlinf{\aidr}{}{\cneg a\lpar a}{\unit}
\vlinf{\pdr}{}
{\nP\connn{\gM_1,\ldots,\gM_n}\lpar \gP\connn{\gM'_1,\ldots,\gM'_n}}
{(M_1\lpar N_1)\ltens \cdots \ltens\, (\gM_n\lpar \gM'_n)}
\\\\
\vlinf{\sdr}{}{\gM_i \lpar \gP\connn{\gM_1, \ldots, \gM_{i-1}, \gN,\gM_{i+1}, \ldots, \gM_n}}{\gP\connn{\gM_1, \ldots, \gM_{i-1}, \gM_i\lpar \gN, \gM_{i+1},\ldots \gM_n}}
\vlinf{\sur}{}{\gP\connn{\gM_1,\ldots, \gM_{i-1},\gM_i \ltens \gN,\gM_{i+1}, \ldots, \gM_n}}{\gM_i\ltens\gP\connn{\gM_1,\ldots,\gM_{i-1}, \gN, \gM_{i+1},\ldots, \gM_n}}
\end{array}
Inference rules for the system $\GS$, where $\gP$ is a prime graph and $\gM_i\neq\unit\neq\gM_i'$ for all $i\in\intset1n$.

The set of rules we consider here is a slightly different formulation of with respect to [4] and [5]:
we consider a $\prule$-rules with a stronger side condition (all factors to be non-empty)
which is balanced by the presence of $\sur$ in the system.
The proof that the formulation we consider in this paper is equivalent to the ones in the literature is provided in <Ref>.

We can easily prove that each sequent provable in $\PMLx$ is interpreted by $\gof\cdot$ as a graph which is admitting a proof in $\GS$.

Let $\Gamma$ be a sequent.
If $\proves[\PMLx]\Gamma$,
then $\proves[\GS]\gof{\Gamma}$.

We define a derivation $\gof\pi$ of $\gof \Gamma$ in $\GS$
by induction by induction on the last rule $\rrule$ in a derivation $\pi$ of $\Gamma$ in $\PMLx$
according to <Ref>.

max width = $\begin{array}{c}
\vlinf{\axrule}{}{\vdash a,\cneg a}{}
\transto
\odiso{\odn{\unit}{\aidr}{a\lpar \cneg a}{}}{\gof{a,\cneg a}}
\qquad
\vlderivation{\vlin{\lparr}{}{\vdash \Delta, \fA\lpar \fB}{\vldr{\pi_1}{\vdash \Delta, \fA,\fB}}}
\transto
\odiso{
\od{\odp{\gof{\pi_1}}{\gof{\Delta, \fA,\fB}}{\IH}}
\gof{\Delta, \fA\lpar\fB}
\qquad
\vlderivation{
\vliin{\ltensr}{}{
\vdash\Delta_1, \Delta_2,\fA\ltens\fB
\vldr{\pi_1}{\vdash\Delta_1, \fA}
\vldr{\pi_n}{\vdash\Delta_2, \fB}
\transto
\odiso{
\odn{
\od{\odp{\gof{\pi_1}}{\odiso{\gof{\Delta_1,  \fA}}{\gof{\Delta_1} \lpar \gof{\fA}}}{\IH}}
\ltens
\od{\odp{\gof{\pi_2}}{\odiso{\gof{\Delta_2,\fB}}{\gof{\Delta_2} \lpar \gof\fB}}{\IH}}
\gof{\Delta_1} \lpar \gof{\Delta_2}
\lpar
\left(\fA\ltens\fB \right)
\gof{\Delta_1 , \Delta_2, \fA \ltens\fB }
\\\\
\vlderivation{\vliiin{\dconr}{}{\vdash \Delta_1,\ldots,\Delta_n, \fP\connn{\fA_1, \ldots, \fA_n},\nfP\connn{\fB_1, \ldots, \fB_n}}
{\vldr{\pi_1}{\vdash \Delta_1, \fA_1, \fB_1}}{\vlhy{\qquad\dots\qquad}}{\vldr{\pi_n}{\vdash \Delta_n, \fA_n, \fB_n}}
\quad \transto\quad
\odiso{\odn{
\od{\odp{\dD_{\pi_1}}{
\odiso{\gof{\Delta_1,\fA_1,\fB_1}}{\gof{\Delta_1} \lpar (\gof{\fA_1}\lpar \gof{\fB_1})}}{\IH}}
\ltens\cdots\ltens
\od{\odp{\dD_{\pi_n}}{
\odiso{\gof{\Delta_n,\fA_n,\fB_n}}{\gof{\Delta_1} \lpar (\gof{\fA_n}\lpar \gof{\fB_n})}}{\IH}}
\mlpar\connn{\gof{\Delta_1}, \ldots ,\gof{\Delta_n}}
\lpar
\odn{
(\gof{\fA_1}\lpar \gof{\fB_1})\ltens \cdots\ltens (\gof{\fA_n}\lpar \gof{\fB_n})
\gP\connn{\gof{\fA_1}, \ldots, \gof{\fA_n}}
\lpar
\nP\connn{\gof{\fB_1}, \ldots, \gof{\fB_n}}
\gof{\Delta_1,\ldots, \Delta_n,\fP\connn{\fA_1, \ldots,  \fA_n},\nfP\connn{\fB_1, \ldots, \fB_n}}
\\\\
\vlderivation{\vliin{\mixr}{}{\vdash \Delta_1,\Delta_2}{\vldr{\pi_1}{\vdash \Delta_1}}{\vldr{\pi_2}{\vdash \Delta_2}}}
\transto
\odiso{
\ods{\unit}{\gof{\pi_1}}{\gof{\Delta_1}}{\IH}
\lpar
\ods{\unit}{\gof{\pi_1}}{\gof{\Delta_2}}{\IH}
\qquad
\vlinf{\unitor}{}{
\vdash \Gamma, \con\connn{\fA_1,\ldots, \fA_k,\funit,\fA_{k+1},\ldots,\fA_n}
\vdash \Gamma,\fC\connn{\fA_{\sigma(1)},\ldots, \fA_{\sigma(n)}}
\transto
\odiso{
\gof{\vdash \Gamma,\fC\connn{\fA_{\sigma(1)},\ldots, \fA_{\sigma(n)}}}
\gof{\Gamma, \con\connn{\fA_1,\ldots, \fA_k,\funit,\fA_{k+1},\ldots,\fA_n}}
\\\\
%		\vlinf{\funit}{}{\vdash\funit,\funit}{}
%		\transto
%		\unit
%		%
%		\qquad
\vlderivation{\vliin{\wdtr}{}{
\vdash \Delta_1,\Delta_2, \fP\connn{\fA_1, \ldots, \fA_n}
\vldr{\pi_1}{\vdash \Delta_1, \fA_1}
\vldr{\pi_2}{\vdash \Delta_n, \fC\connn{\fA_2,\ldots, \fA_n}}
\quad \transto\quad
\odiso{
\odn{
\od{\odp{\dD_{\pi_1}}{\odiso{\gof{\Delta_1,\fA_1}}{\gof{\Delta_1} \lpar \gof{\fA_1} }}{\IH}}
\ltens
\od{\odp{\dD_{\pi_2}}{\odiso{\gof{\Delta_2,\fC\connn{\fA_2,\ldots, \fA_n}}}{\gof{\Delta_1} \lpar \gof{\fC\connn{\fA_2,\ldots, \fA_n}}}}{\IH}}
\left(\gof{\Delta_1}\lpar \gof{\Delta_2}\right)
\lpar
\odiso{\gof{\fA_1}\ltens \gof{\fC\connn{\fA_2, \ldots, \fA_n}}}{
\odn{\gof{\fA_1}\ltens \gof{\fC}\connn{\gof{\fA_2}, \ldots, \gof{\fA_n}}}{\sur}{
\gP\connn{\gof{\fA_1}, \ldots,  \gof{\fA_n}}
\gof{\Delta_1, \Delta_2,\fP\connn{\fA_1, \ldots,  \fA_n}}
\end{array}$
Rules to translate derivations in $\PMLx$ into derivations in $\GS$.

To prove the converse, we use the admissibility of $\wdpr$ to prove that
every time there is a rule in $\GS$ with premise $\gH$ and conclusion $\gG$,
then there are formulas $\fA$ and $\fB$ such that $\gof\fA$ and $\gof\fB$, and such that $\fB\limp \fA$.

Let $\rrule\in\set{\sdr,\sur,\pdr}$.
If $\vlinf{\rrule}{}{\gG}{\gH}$,
then there are formulas
$\fA$ and $\fB$ with
$\gof\fA={\gG}$ and $\gof\fB={\gH}$
such that
$\proves[\PMLx]\cneg\fB, \fA$.

We first discuss the case if $\cC\conso=\chole$:

* if $\rrule=\sdr$, then
$\fA=\fM_i\lpar \con\connn{\fM_1, \ldots, \fM_{i-1}, \funit\lpar\fN, \fM_{i+1},\ldots \fM_n}$
$\fB=\con\connn{\fM_1, \ldots, \fM_{i-1}, \fM_i\lpar \fN, \fM_{i+1},\ldots \fM_n}$
for some formulas $\mu_1,\ldots,\mu_n,\nu$ such that $\gof{\fM_i}=\gM_i$ for all $i\in\intset1n$ and $\gof\fN=\gN$.
We conclude by <Ref> since we have the following derivation

\vlin{\lpar}{}{
\vdash
\cneg\fB, \fA
\vdash
\cneg{\fB}, \fM_i , \con\connn{\fM_1, \ldots, \fM_{i-1}, \funit \lpar \fN,\fM_{i+1}, \ldots, \fM_n}
\vlin{\AXrule}{}{
\vdash\cneg\fB, \con\connn{\fM_1, \ldots, \fM_{i-1}, \fM_i \lpar \fN,\fM_{i+1}, \ldots, \fM_n}}{\vlhy{}}

* if $\rrule=\sur$ then
$\fA=\con\connn{\fM_1, \ldots, \fM_{i-1}, \fM_i\ltens\fN, \fM_{i+1},\ldots \fM_n}$
$\fB= \fM_i\ltens \con\connn{\fM_1, \ldots, \fM_{i-1}, \funit\ltens \fN, \fM_{i+1},\ldots \fM_n}$
for some formulas $\mu_1,\ldots,\mu_n,\nu$ such that $\gof{\fM_i}=\gM_i$ for all $i\in\intset1n$ and $\gof\fN=\gN$.
We conclude by <Ref> since we have the following derivation

\vlderivation{
\vlin{\lpar}{}{
\vdash
\cneg\fB, \fA
\vdash
\nfM_i, \ncon\connn{\nfM_1, \ldots, \nfM_{i-1},  \funit\lpar\nfN, \nfM_{i+1},\ldots \nfM_n}
\fA
\vlin{\AXrule}{}{
\vdash
\ncon\connn{\nfM_1, \ldots, \nfM_{i-1}, \nfM_i\lpar\nfN, \nfM_{i+1},\ldots \nfM_n}
\fA

* if $\rrule=\pdr$ then
$\fA=\nfP\connn{\fM_1,\ldots,\fM_n}\lpar \fP\connn{\fN_1,\ldots,\fN_n}$
$\cneg\fB=(\cneg\fM_1\ltens \cneg\fN_1)\lpar \cdots \lpar(\cneg\fM_n\ltens \cneg\fN_n)$
for some formulas
$\mu_1,\ldots,\mu_n,\nu_1,\ldots, \nu_n$ such that $\gof{\fM_i}=\gM_i\neq\unit$ and $\gof{\fN_i}=\gN_i\neq\unit$ for all $i\in\intset1n$.
We conclude since we have the following derivation

\vlderivation{
\vliq{\lpar}{}{
(\cneg\fM_1\ltens \cneg\fN_1)
\lpar \cdots \lpar
(\cneg\fM_n\ltens \cneg\fN_n)
\fA
\vliiin{\dconr}{}{
\vdash
(\cneg\fM_1\ltens \cneg\fN_1)
, \ldots ,
(\cneg\fM_n\ltens \cneg\fN_n),
\fA
\vliin{\ltens}{}{\vdash\cneg\fM_1\ltens \cneg\fN_1 , \fM_1,\fN_1}{\vlin{\AXrule}{}{\vdash \fM_1 ,\cneg\fM_1}{\vlhy{}}}{\vlin{\AXrule}{}{\vdash \fN_1 ,\cneg\fN_1}{\vlhy{}}}
\vlhy{\;\cdots\;}
\vliin{\ltens}{}{\vdash\cneg\fM_n\ltens \cneg\fN_n , \fM_n,\fN_n}{\vlin{\AXrule}{}{\vdash \fM_n ,\cneg\fM_n}{\vlhy{}}}{\vlin{\AXrule}{}{\vdash \fN_n ,\cneg\fN_n}{\vlhy{}}}

$\cC\conso=\con[\gP]\connn{\cC'\conso, \gM_1, \ldots, \gM_n}\neq\chole$, then we assume w.l.o.g.,
there is a context formula
$\fcC\conso=\fP\connn{\fcC'\conso, \fM_1, \ldots, \fM_n}$
such that
$\gof{\fcC\conso}=\cC\conso$ and $\gof{\fcC'\conso}=\cC'\conso$ .
We conclude since, by inductive hypothesis on the structure of $\cC\conso$, there is a derivation of the following form:

\vlderivation{
\vliiiin{\dconr}{}{
\vdash
\nfP\Connn{\cneg{\left(\fcC'\cons{\fB'}\right)}, \nfM_1, \ldots, \nfM_n}
\fP\Connn{\fcC'\cons{\fA'}, \fM_1, \ldots, \fM_n}
\vlpr{}{\IH}{\vdash \cneg{\left(\fcC'\cons{\fB'}\right)} , \fcC'\cons{\fA'}}
\vlin{\AXrule}{}{\vdash \cneg\fM_1, \fM_1}{\vlhy{}}
\vlhy{\cdots}
\vlin{\AXrule}{}{\vdash \cneg\fM_n, \fM_n}{\vlhy{}}
\qquad.

We are now able to prove the main result of this section, that is, establishing a correspondence between graphs provable in $\GS$ and graphs which are interpretation via $\gof\cdot$ of formulas provable in $\PMLx$.

Let $\gG\neq\unit$ be a graph and $\fA$ a pure formula such that $\gof\fA=\gG$.
$\proves[\GS]\gG$ iff $\proves[\PMLx]\fA$.

By  <Ref>, if $\proves[\PMLx]\fA$, then by there is a proof of $\gof\fA$ in $\PMLx$.

To prove the converse, let $\dD$ be a proof of $\gG\neq\unit$ in $\GS$.
We define a proof $\pi_\dD$ of $\fA$
by induction on the number $n$ of rules in $\dD$.

* We cannot have $n=0$ since we are assuming $\gG\neq\unit$.

* If $n=1$, then $\gG=a\lpar \cneg a$
$\pi_\dD=\vlsmash{\vlderivation{\vlin{\lpar}{}{\vdash a\lpar \cneg a}{\vlin{\axrule}{}{\vdash a, \cneg a}{\vlhy{}}}}}$

* If $n>1$, then $\dD=\odn{\od{\odp{\dD'}{\gH}{}}}{\rrule}{\gG}{}$
then by inductive hypothesis
we have a proof $\pi_{\dD'}$ of a formula $\fB$ such that

If $\rrule\in\set{\sdr,\sur,\pdr}$, then by  <Ref>
we have a derivation with $\cutr$ as the one below on the left of a formula $\fA$ such that $\gof\fA=\gG$.
We then conclude by <Ref>.

\vlderivation{
\vliin{\cutr}{}{\vdash \fA}{\vlpr{}{\IH}{\psi}}{\vlpr{}{\text{\Cref{lem:DrulesCons}}}{\vdash \cneg\fB, \fA}}
\quad\overset{\Cref{thm:cutelim}}{\rightsquigarrow^*}\quad
\vlderivation{\vlpr{}{\PMLx}{\fA}}
\qquad\quad&\quad\qquad
\vlderivation{
\vlid{=}{}{
\vdash \fA
\vliin{\deepr}{}{
\vdash \fcC\cons{a\lpar\cneg a}
\vlin{\lparr}{}{\vdash a\lpar \cneg a}{\vlin{\axrule}{}{\vdash a, \cneg a}{\vlhy{}}}
\vlpr{\pi_{\dD'}}{\IH}{\fB}
\end{array}$$

Otherwise $\rrule=\aidr$, then it must have been applied deep inside a context
$\cC\conso=\gof{\fcC\conso}\neq\chole$ such that $\cC\consu=\gH=\gof{\fB}$.
Therefore $\fA=\fcC\cons{a\lpar\cneg a}$.
We conclude by applying
<Ref> to the derivation above on the right.

§ CLASSICAL LOGIC BEYOND COGRAPHS

We conclude this paper by providing an extension of $\PML$ with standard contraction and weakening structural rules, showing that it provides a conservative extension of propositional classical logic.
We then show decomposition results allowing us to factorize any proof into a linear proof (i.e., a proof in $\PML$) and a resource management proof (i.e., a derivation only using weakening and contraction rules).

We define the following sequent system:

\begin{equation}\label{eq:LKsys}
\begin{array}{l@{\colon\;}l@{\;=\;}l}
\mbox{\defn{Classical Graphical  Logic}}
\PLK
\PML\cup\set{\wrule,\crule}
%			\\
%			\mbox{\defn{Classical Graphical  Logic}}
%			&
%			\GLK
%			&
%			\Set{\gof \fA\mid \fA \mbox{ formula such that }\proves[\PLK]\fA}
\end{array}
\end{equation}

max width=$\begin{array}{c}
\begin{array}{c@{\qquad}|@{\qquad}c@{\qquad}|@{\qquad}c}
\vlinf{\wrule}{}{\vdash \Gamma, \fA}{\vdash\Gamma}
\qquad
\vlinf{\crule}{}{\vdash \Gamma, \fA}{\vdash\Gamma, \fA, \fA}
\vlinf{\dwrule}{}{\fB\lpar\fA}{\fB}
\qquad
\vlinf{\dcrule}{}{\fA}{\fA\lpar \fA}
\vlinf{\dacrule}{}{a}{a \lpar a}
\qquad
\vlinf{\medr}{\text{\scriptsize$\lpar\neq\gP$ prime}}{\gP\connn{\fA_1\lpar \fB_1,\ldots, \fA_n\lpar \fB_n}}{
\gP\connn{\fA_1,\ldots, \fA_n}\lpar	\gP\connn{\fB_1,\ldots, \fB_n}
\end{array}
\end{array}$
Structural rules for sequent calculi, and the corresponding rules in deep inference together with the atomic contraction and the generalized medial rule.

For $\PLK$ we can prove the admissibility of the $\cutr$-rule via cut-elimination.

The rule $\cutr$ is admissible in $\PLK$.

Consider the cut-elimination steps from <Ref> and <Ref>
and the definition of weight from the proof of <Ref>.
A proof of weak normalization of the cut-elimination procedure can be given using the same measure used in the proof of <Ref>
For the sake of determining if a cut-formula is principal,
in a contraction rule ($\crule$) we assume both occurrences of $\fA$ in the premise to be active and the occurrence of $\fA$ in the conclusion to be principal.
by restraining the application of the cut-elimination steps only to top-most $\cutr$-rules in the derivation.

max width=$\begin{array}{c}
\vlderivation{
\vliin{\cutr}{}{\vdash \Gamma, \Delta}{
\vlin{\wrule}{}{\vdash \Gamma,\fA}{
\vlhy{\vdash \Gamma}}
\vlhy{\vdash \nfA, \Delta}
\;\rightsquigarrow\;
\vlderivation{\vliq{\wrule}{}{\vdash \Gamma,\Delta}{
\vlhy{\vdash \Gamma}}}
\qquad\qquad
\vlderivation{
\vliin{\cutr}{}{\vdash \Gamma, \Delta}{
\vlin{\crule}{}{\vdash \Gamma, \fA}{
\vlhy{\vdash \Gamma, \fA, \fA}}
\vlhy{\vdash  \nfA , \Delta}
\;\rightsquigarrow\;
\vlderivation{
\vliq{\crule}{}{\vdash \Gamma, \Delta}{
\vliin{\cutr}{}{\vdash \Gamma, \Delta, \Delta}{
\vliin{\cutr}{}{\vdash \Gamma, \Delta, \fA}{
\vlhy{\vdash \Gamma, \fA, \fA}
\vlhy{\vdash  \nfA , \Delta}
\vlhy{\vdash  \nfA , \Delta}
\end{array}$
The cut-elimination steps for the structural rules.

We consider the deep inference rules in <Ref>, that is, rules which can be applied on subformulas in a sequent.
the deep inference version of the structural rules (weakening and contraction) and the
generalized medial rule proposed in [18]
we can define a inference system
where structural rules can pushed down in a derivation
obtaining a decomposition result extending the one in
[14, 16] for classical logic.

The contraction rule $\dcrule$ is derivable using atomic contraction ($\dacrule$) and medial rule ($\medr$).

By induction on the contracted formula $\fA$.
If $\fA=a$ is an atom, then $\dcrule$ is an instance of $\dacrule$.
Otherwise, $\fA=\con\connn{\fB_1,\ldots, \fB_n}$ and
we conclude since we can apply inductive hypothesis
to replace each application of $\dcrule$ with a derivation of the following form

\odn{\con\connn{\fB_1,\ldots, \fB_n}\lpar \con\connn{\fB_1,\ldots, \fB_n}}{\dcrule}{
\con\Connn{\fB_1,\ldots, \fB_n}
\qquad\rightsquigarrow\qquad
\odn{\con\connn{\fB_1,\ldots, \fB_n}\lpar \con\connn{\fB_1,\ldots, \fB_n}}{\medr}{
\con\Connn{\ods{\fB_1\lpar \fB_1}{\IH}{\fB_1}{\set{\medr,\dacrule}},\ldots, \ods{\fB_n\lpar \fB_n}{\IH}{\fB_n}{\set{\medr,\dacrule}}}
\; .

Let $\Gamma$ be a sequent.
If $\proves[\PLK]\Gamma$,

there is a sequent $\Gamma'$ such that
%		$ and $\Gamma'
\proves[\set{\dwrule,\dcrule}]\Gamma$

there are sequent $\Gamma'$, $\Delta'$, and $\Delta$
such that
%		$ and  $\Gamma'
\proves[\set{\medr}]\Delta'
%		$ and$\Gamma_1
\proves[\set{\dacrule}]\Delta
%		$ and $\Gamma_2
\proves[\set{\dwrule}]\Gamma$

The proof of <Ref> is immediate by applying rule permutations.
For a reference, see [7].
<Ref> is consequence of the previous point
since by <Ref> we can replace all instances of $\dcrule$-rules with derivations containing only $\medr$ and $\dacrule$, and conclude by applying rule permutations to move all $\acrule$-rules below the instances of $\medr$-rules, and $\dwrule$ to the bottom of a derivation.

To conclude this section, we recall that classical graphical logic, is not the same logic of the boolean graphical logic (denoted $\GBL$) defined in [18] (an inference systems on graphs by extending the semantics of read-once boolean relations from cographs to general graphs).
In fact, even if both are conservative extensions of classical logic,
the following graph from [5] which is expected to be provable in $\GBL$,
but is not provable in $\GS$ (and there is no formula $\fA$ provable in $\PLK$ such that $\gof\fA$ is the given graph).

\begin{array}{cc@{\quad}cc}
&\vb1& \vnc1&		\\
\va1&	 &		&\vnb1	\\
\end{array}
\Gedges{a1/b1,b1/nc1,nc1/nb1,nb1/na1,na1/c1,a1/c1}

§ CONCLUSION AND FUTURE WORKS

In this paper we have provided foundations for the design of proof systems operating on graph by defining graphical connectives,
a class of logical operators generalizing the classical conjunction and disjunction,
whose semantics is solely defined by their interpretation as prime graphs.

We studied two sub-structural sequent calculi operating on formulas defined via graphical connectives ($\PML$ and $\PMLx$), proving that cut-elimination holds in these systems and that they are conservative extensions of
the multiplicative linear logic and the multiplicative linear logic with mix respectively.

For these calculi, we proved that they capture graph isomorphisms as provable logical equivalences
Note that the sequent calculus is only capable of checking if two graphs sharing the same set of vertices are isomorphic (problem with polynomial complexity), but not to find an correspondence between vertices of two graphs which is an isomorphism (a well-known $\NP$ problem)
We were able to prove that the class of graphs representing provable formulas in $\PMLx$
coincides with
the class of non-empty graphs provable in the proof system $\GS$ from [4, 3].
As a consequence, the proofs of cut-elimination in $\PML$ serves as simplified version of the proof of transitivity of implication in $\GS$.

We concluded by providing a conservative extension of both classical propositional logic and $\PML$,
and proving the existence of a decomposition result allowing us to have canonical forms for proofs in which all structural rules can be relegated at the bottom of a derivation.

§.§ Future Works

Categorical Semantics

Unit-free star-autonomous and IsoMix categories [19, 20] provide categorical models of $\MLL$ and $\MLLx$ respectively.
We conjecture that categorical models for $\PML$ and $\PMLx$ can be defined by enriching such structures with additional $n$-ary monoidal products and natural transformation, reflecting the symmetries observed in the symmetry groups of prime graphs.

Digraphs, Games and Event Structures

In this work we have extended the correspondence between classical propositional and cographs from [21] to the case of general (undirected) graphs using graphical connectives. The same idea can be found in [2] for mixed graphs.
A similar generalization of the correspondence between intuitionistic propositional formulas and arenas used in Hyland-Ong game semantics [41]. Arenas are directed graphs characterized by the absence of specific induced subgraphs.
We foresee the possibility of defining conservative extensions of intuitionistic propositional logic beyond arenas, analogously as what done in this paper, where we provided conservative extensions of classical propositional logic beyond cographs.
Such proof systems would provide new insights on the proof theory connected to concurrent games [1, 58, 65], and could be used to define automated tools operating on event structures [55].

btensaa b

\begin{array}{c|c}
\begin{array}{c@{\qquad}c}
\\
\begin{array}{cc}
\vnb1\;\; \vna1\;\;\; & \;\;\; \va1 \quad \vb1
\\
\Gpar1&\Gtens1
\\[5pt]
\vnbtensa1
\vbtensa1
\end{array}
\pswires{Gpar1.O/nbtensa1,Gtens1.O/btensa1}
\psaxioms{Gpar1.R/Gtens1.L,Gpar1.L/Gtens1.R}
\begin{array}{c@{\;}c@{\;}cc@{\;}c@{\;}c}
\vnb1 &&  \vna1 & \va1 && \vb1
\\
&\vvo{\lpar}1&&& \vvo{\ltens}2
\\[5pt]
&\vvr{\lpar}1&&& \vvr{\ltens}2
\end{array}
\Bedges{vo1/vr1,vo2/vr2}
\Redges{a1/b1}
\multiRedges{a1,b1}{vo2}
\multiRedges{na1,nb1}{vo1}
\sqBedges{a1/na1/10,nb1/b1/15}
\end{array}
\begin{array}{cc}
\\
\begin{array}{c}
\vnc1 \quad \vna1	\quad\vnd1	\quad\vnb1
\\[5pt]
\vvo{\nPfour}2
\\[5pt]
\vvr{\nPfour}2
\end{array}
\begin{array}{c}
\va1\quad \vb1 \quad \vc1 \quad \vd1
\\[5pt]
\vvo{\Pfour}1
\\[5pt]
\vvr{\Pfour}1
\end{array}
\end{array}
\Hpath{
++(0,20pt)	-|
(a1.center)	--
(b1.center)	--
++(0,16pt)	-|
++(0,8pt)	-|
(d1.center)	--
(c1.center)	--
++(0,12pt)	-|
\Redges{a1/b1,b1/c1,c1/d1}
\Redges{nc1/na1,nd1/nb1,na1/nd1}
\multiRedges{vo1}{a1,b1,c1,d1}
\multiRedges{vo2}{na1,nb1,nc1,nd1}
\sqBedges{a1/na1/20,b1/nb1/16,c1/nc1/12,d1/nd1/8}
\Bedges{vo1/vr1,vo2/vr2}
\end{array}

On the left: the same proof net in the original Girard's syntax and Retoré's one.
On the right: an of $\fcon{\Pfour}\connn{a,b,c,d}\limp \fcon{\Pfour}\connn{a,b,c,d}$ containing the chorded æ-cycle $a\cdot b \cdot \cneg b\cdot \cneg d \cdot d \cdot c \cdot \cneg c\cdot \cneg a$.

Proof nets and automated proof search

We plan to design proof nets [29, 22, 30] for $\PML$ and $\PMLx$, as well as combinatorial proofs [40] for $\PLK$.
For this purpose, we envisage to extend Retoré's handsome proof net syntax, where proof nets are represented by two-colored graphs (see the left of <Ref>). In Retoré's syntax, the graph induced by the vertices corresponding to the inputs of a $\lpar$-gate (or a $\ltens$-gate) is similar to the corresponding prime graph $\lpar$ (resp. $\ltens$). Thus, gates for graphical connectives could be easily defined by extending this correspondence (see the proof net on the right of <Ref>).

The standard correctness condition defined via acyclicity would fails for these proof nets, as shown in the right-hand side of <Ref>: the (correct) proof-net of the sequent $\Pfour\connn{a,b,c,d}\limp \Pfour\connn{a,b,c,d}$ contains a cycle.
We foresee the possibility of using results on the primeval decomposition of graphs [43, 38] to isolate those cycles witnessing unsoundness, as proposed in [52].
Such a result would open to the possibility of defining combinatorial proofs [40, 39] for $\PLK$ relying on the decomposition result (<Ref>), and may provide a methodology to find machine-learning guided automated theorem provers for $\PML$ and $\PMLx$ using the methods in [44].

[1]
Samson Abramsky and P-A Mellies.
Concurrent games and full completeness.
In Proceedings. 14th Symposium on Logic in Computer Science
(Cat. No. PR00158), pages 431–442. IEEE, 1999.

[2]
Matteo Acclavio, Ross Horne, Sjouke Mauw, and Lutz Straßburger.
A Graphical Proof Theory of Logical Time.
In Amy P. Felty, editor, 7th International Conference on Formal
Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages
22:1–22:25, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum
für Informatik.

[3]
Matteo Acclavio, Ross Horne, and Lutz Straßburger.
An Analytic Propositional Proof System On Graphs.
This is an extended version of a paper published at LICS 2020
[AHS20]., December 2020.

[4]
Matteo Acclavio, Ross Horne, and Lutz Straßburger.
Logic beyond formulas: A proof system on graphs.
In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS '20, page 38–52, New York, NY, USA, 2020.
Association for Computing Machinery.

[5]
Matteo Acclavio, Ross Horne, and Lutz Straßburger.
An Analytic Propositional Proof System on Graphs.
Logical Methods in Computer Science, Volume 18, Issue 4,
October 2022.

[6]
Matteo Acclavio and Roberto Maieli.
Generalized connectives for multiplicative linear logic.
In Maribel Fernández and Anca Muscholl, editors, 28th EACSL
Annual Conference on Computer Science Logic (CSL 2020), volume 152 of LIPIcs, pages 6:1–6:16, Dagstuhl, Germany, 2020. Schloss
Dagstuhl–Leibniz-Zentrum fuer Informatik.

[7]
Matteo Acclavio and Lutz Straßburger.
From syntactic proofs to combinatorial proofs.
In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors,
Automated Reasoning - 9th International Joint Conference, IJCAR 2018,
Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July
14-17, 2018, Proceedings, volume 10900, pages 481–497. Springer, 2018.

[8]
Andrea Aler Tubella and Alessio Guglielmi.
Subatomic proof systems: Splittable systems.
ACM Trans. Comput. Logic, 19(1), January 2018.

[9]
Andrea Aler Tubella and Lutz Straßburger.
Introduction to Deep Inference.
Lecture, August 2019.

[10]
Jean-Marc Andreoli.
Logic programming with focusing proofs in linear logic.
Journal of Logic and Computation, 2(3):297–347, 1992.

[11]
Arnon Avron and Iddo Lev.
Canonical propositional Gentzen-type systems.
In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors,
Automated Reasoning, pages 529–544, Berlin, Heidelberg, 2001. Springer
Berlin Heidelberg.

[12]
László Babai.
Graph isomorphism in quasipolynomial time [extended abstract].
In Proceedings of the Forty-Eighth Annual ACM Symposium on
Theory of Computing, STOC '16, page 684–697, New York, NY, USA, 2016.
Association for Computing Machinery.

[13]
Patrick Blackburn, Maarten De Rijke, and Yde Venema.
Modal logic: graph. Darst, volume 53.
Cambridge University Press, 2001.

[14]
Kai Brünnler.
Locality for classical logic.
Notre Dame Journal of Formal Logic, 47(4):557–580, 2006.

[15]
Kai Brünnler and Lutz Straßburger.
Modular sequent systems for modal logic.
In Martin Giese and Arild Waaler, editors, Automated Reasoning
with Analytic Tableaux and Related Methods, TABLEAUX'09, volume 5607 of Lecture Notes in Computer Science, pages 152–166. Springer, 2009.

[16]
Paola Bruscoli and Lutz Straßburger.
On the length of medial-switch-mix derivations.
In Juliette Kennedy and Ruy J. G. B. de Queiroz, editors, Logic,
Language, Information, and Computation - 24th International Workshop, WoLLIC
2017, London, UK, July 18-21, 2017, Proceedings, volume 10388 of Lecture Notes in Computer Science, pages 68–79. Springer, 2017.

[17]
Cameron Calk.
A graph theoretical extension of boolean logic.
Bachelor's thesis, 2016.

[18]
Cameron Calk, Anupam Das, and Tim Waring.
Beyond formulas-as-cographs: an extension of boolean logic to
arbitrary graphs, 2020.

[19]
J.R.B. Cockett and R.A.G. Seely.
Proof theory for full intuitionistic linear logic, bilinear logic,
and mix categories.
Theory and Applications of Categories, 3(5):85–131, 1997.

[20]
J.R.B. Cockett and R.A.G. Seely.
Weakly distributive categories.
J. of Pure and Applied Algebra, 114:133–173, 1997.

[21]
D.G. Corneil, H. Lerchs, and L.Stewart Burlingham.
Complement reducible graphs.
Discrete Applied Mathematics, 3(3):163–174, 1981.

[22]
Vincent Danos and Laurent Regnier.
The structure of multiplicatives.
Archive for Mathematical logic, 28(3):181–203, 1989.

[23]
Anupam Das.
Complexity of evaluation and entailment in boolean graph logic.
preprint, 2019.

[24]
Anupam Das and Alex A. Rice.
New minimal linear inferences in boolean logic independent of switch
and medial.
In Naoki Kobayashi, editor, 6th International Conference on
Formal Structures for Computation and Deduction, FSCD 2021, July 17-24,
2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 14:1–14:19. Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2021.

[25]
Pierre-Malo Deniélou and Nobuko Yoshida.
Buffered communication analysis in distributed multiparty sessions.
In Paul Gastin and François Laroussinie, editors, CONCUR
2010 - Concurrency Theory, pages 343–357, Berlin, Heidelberg, 2010.

[26]
A. Ehrenfeucht, T. Harju, and G Rozenberg.
The Theory of 2-Structures A Framework for Decomposition and
Transformation of Graphs.
World Scientific, 1999.

[27]
Xiang Fu, Tevfik Bultan, and Jianwen Su.
Analysis of interacting BPEL web services.
In Proceedings of the 13th international conference on World
Wide Web, pages 621–630. ACM, 2004.

[28]
Tibor Gallai.
Transitiv orientierbare Graphen.
Acta Mathematica Academiae Scientiarum Hungarica,
18(1–2):25–66, 1967.

[29]
Jean-Yves Girard.
Linear logic.
Theoretical Computer Science, 50:1–102, 1987.

[30]
Jean-Yves Girard.
Proof-nets : the parallel syntax for proof-theory.
In Aldo Ursini and Paolo Agliano, editors, Logic and Algebra.
Marcel Dekker, New York, 1996.

[31]
Jean-Yves Girard.
Light linear logic.
Information and Computation, 143:175–204, 1998.

[32]
Jean-Yves Girard.
On the meaning of logical rules II: multiplicatives and additives.
NATO ASI Series F: Computer and Systems Sciences, 175:183–212,

[33]
Alessio Guglielmi.
A system of interaction and structure.
ACM Transactions on Computational Logic, 8(1):1–64, 2007.

[34]
Alessio Guglielmi, Tom Gundersen, and Michel Parigot.
A proof calculus which reduces syntactic bureaucracy.
In Christopher Lynch, editor, Proceedings of the 21st
International Conference on Rewriting Techniques and Applications, volume 6
of LIPIcs, pages 135–150, Dagstuhl, Germany, 2010. Schloss
Dagstuhl–Leibniz-Zentrum fuer Informatik.

[35]
Alessio Guglielmi and Lutz Straßburger.
Non-commutativity and MELL in the calculus of structures.
In Laurent Fribourg, editor, Computer Science Logic, pages
54–68, Berlin, Heidelberg, 2001. Springer.

[36]
Alessio Guglielmi and Lutz Straßburger.
A non-commutative extension of MELL.
In Matthias Baaz and Andrei Voronkov, editors, Logic for
Programming, Artificial Intelligence, and Reasoning, pages 231–246, Berlin,
Heidelberg, 2002. Springer.

[37]
Michel Habib and Christophe Paul.
A survey of the algorithmic aspects of modular decomposition.
Computer Science Review, 4(1):41–59, 2010.

[38]
Stefan Hougardy.
On the P4-structure of perfect graphs.
Citeseer, 1996.

[39]
Dominic Hughes.
Proofs Without Syntax.
Annals of Mathematics, 164(3):1065–1076, 2006.

[40]
Dominic Hughes.
Towards Hilbert's 24\({}^{\mbox{th}}\) problem: Combinatorial proof
invariants: (preliminary version).
Electr. Notes Theor. Comput. Sci., 165:37–63, 2006.

[41]
J. Martin E. Hyland and Chih-Hao Luke Ong.
On full abstraction for PCF: I. Models, observables and the
full abstraction problem, II. Dialogue games and innocent strategies,
III. A fully abstract and universal game model.
Information and Computation, 163:285–408, 2000.

[42]
Lee O James, Ralph G Stanton, and Donald D Cowan.
Graph decomposition for undirected graphs.
In Proceedings of the Third Southeastern Conference on
Combinatorics, Graph Theory, and Computing (Florida Atlantic Univ., Boca
Raton, Fla., 1972), pages 281–290, 1972.

[43]
Beverly Jamison and Stephan Olariu.
P-components and the homogeneous decomposition of graphs.
SIAM Journal on Discrete Mathematics, 8(3):448–463, 1995.

[44]
Konstantinos Kogkalidis, Michael Moortgat, and Richard Moot.
Neural proof nets.
In Raquel Fernández and Tal Linzen, editors, Proceedings of
the 24th Conference on Computational Natural Language Learning, pages
26–40, Online, November 2020. Association for Computational Linguistics.

[45]
Björn Lellmann and Elaine Pimentel.
Modularisation of sequent calculi for normal and non-normal
ACM Trans. Comput. Logic, 20(2), feb 2019.

[46]
László Lovász and Michael D Plummer.
Matching theory, volume 367.
American Mathematical Soc., 2009.

[47]
Saunders Mac Lane.
Categories for the Working Mathematician.
Number 5 in Graduate Texts in Mathematics. Springer, 1971.

[48]
Roberto Maieli.
Non decomposable connectives of linear logic.
Annals of Pure and Applied Logic, 170(11):102709, 2019.

[49]
Ross M. McConnell and Jeremy P. Spinrad.
Linear-time modular decomposition and efficient transitive
orientation of comparability graphs.
In Proceedings of the Fifth Annual ACM-SIAM Symposium on
Discrete Algorithms, SODA '94, pages 536–545, USA, 1994. Society for
Industrial and Applied Mathematics.

[50]
Dale Miller and Elaine Pimentel.
A formal framework for specifying sequent calculus proof systems.
Theoretical Computer Science, 474:98–116, 2013.

[51]
Dale Miller and Alexis Saurin.
From proofs to focused proofs: a modular proof of focalization in
linear logic.
In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer
Science Logic, volume 4646 of LNCS, pages 405–419. Springer-Verlag,

[52]
Lê Thành Dũng Nguyên and Thomas Seiller.
Coherent interaction graphs: A non-deterministic geometry of
interaction for mll.

[53]
Lê Thành Dũng Nguyên and Lutz Straßburger.
A System of Interaction and Structure III: The Complexity of BV and
Pomset Logic.
working paper or preprint, 2022.

[54]
Lê Thành Dũng Nguyên and Lutz Straßburger.
BV and Pomset Logic are not the same.
In Florin Manea and Alex Simpson, editors, 30th EACSL Annual
Conference on Computer Science Logic (CSL 2022), volume 216 of Leibniz
International Proceedings in Informatics (LIPIcs), pages 3:1–3:17,
Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für

[55]
Mogens Nielsen, Gordon Plotkin, and Glynn Winskel.
Petri nets, event structures and domains, part i.
Theoretical Computer Science, 13(1):85–108, 1981.

[56]
Vaughan Pratt.
Modeling concurrency with partial orders.
International journal of parallel programming, 15:33–71, 1986.

[57]
Christian Retoré.
Pomset logic: The other approach to noncommutativity in logic.
Joachim Lambek: The Interplay of Mathematics, Logic, and
Linguistics, pages 299–345, 2021.

[58]
Silvain Rideau and Glynn Winskel.
Concurrent strategies.
In 2011 IEEE 26th Annual Symposium on Logic in Computer
Science, pages 409–418. IEEE, 2011.

[59]
R.A.G. Seely.
Linear logic, *-autonomous categories and cofree coalgebras.
Contemporary Mathematics, 92, 1989.

[60]
Alwen Fernanto Tiu.
A system of interaction and structure II: The need for deep
Logical Methods in Computer Science, 2(2):1–24, 2006.

[61]
Anne Sjerp Troelstra and Helmut Schwichtenberg.
Basic Proof Theory.
Cambridge University Press, second edition, 2000.

[62]
Jacobo Valdes, Robert E Tarjan, and Eugene L Lawler.
The recognition of series parallel digraphs.
In Proceedings of the eleventh annual ACM symposium on Theory of
computing, pages 1–12. ACM, 1979.

[63]
Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, and Alexandra Silva.
Learning pomset automata.
In Stefan Kiefer and Christine Tasson, editors, Foundations of
Software Science and Computation Structures, pages 510–530, Cham, 2021.
Springer International Publishing.

[64]
Timothy Waring.
A graph theoretic extension of boolean logic.
Master's thesis, 2019.

[65]
Glynn Winskel, Silvain Rideau, Pierre Clairambault, and Simon Castellan.
Games and strategies as event structures.
Logical Methods in Computer Science, 13, 2017.

§ DEEP INFERENCE AND THE OPEN DEDUCTION FORMALISM

Open deduction [34] is a proof formalism based on deep inference [9]. It has originally been defined for formulas, but it is abstract enough such that it can equally well be used for graphs, as already done in [3].

An inference system $\sysS$ is a set of inference rules (as for example shown in <Ref>).

A derivation $\dD$ in $\sysS$ with premise $\gG$ and
conclusion $\gH$ is denoted $\vldownsmash{\od{\odd{\odh{\gG}}{\dD}{\gH}{\sysS}}}$
and is defined inductively as follows:

* Every graph $\gG$ is a (trivial) derivation
premise $\gG$ and conclusion $\gG$ (also denoted $\gG$).

* An instance of a rule $\vlinf{\rrule}{}{\gH}{\gG}$  in $ \sysS$ is a derivation with premise $\gG$ and conclusion $\gH$.

* If
$\dD_1$ is a derivation with premise $\gG_1$ and conclusion $\gH_1$,
$\dD_2$ is a derivation with premise $\gG_2$ and conclusion $\gH_2$,
then the composition
of $\dD_1$ and $\dD_2$
is a derivation $\dD_2\comp\dD_1$ denoted as below.

\begin{equation*}\label{eq:iso}
\odiso{
\ods{\gG_1}{\dD_1}{\gH_1}{\sysS}
\ods{\gG_2}{\dD_2}{\gH_2}{\sysS}
\mbox{ or }
\ods{\odiso{\ods{\gG_1}{\dD_1}{\gH_1}{\sysS}}{\gG_2}}{\dD_2}{\gH_2}{\sysS}
\mbox{ or }
\ods{\gG_1}{\dD_1}{\odiso{\gH_1}{\ods{\gG_2}{\dD_2}{\gH_2}{\sysS}}}{\sysS}
\mbox{ or }
\od{\odd{\odd{\odh{\gG_1}}
\mbox{ or }
\od{\odd{\odd{\odh{\gG_1}}
\end{equation*}

Note that even if the symmetry between $\gG_2$ and $\gH_1$ is not written, we always assume it is part of the derivation and explicitly

* If $\gG$ is a graph with $n$ vertices and
$\dD_1,\dots,\dD_n$ are derivations with premise $\gG_i$ and conclusion
$\gH_i$  for each $i\in\intset1n$,
then $\gG\connn{\dD_1,\dots, \dD_n}$ is a derivation with
premise $\gG\connn{\gG_1,\dots, \gG_n}$
and conclusion $\gG\connn{\gH_1,\dots, \gH_n}$
denoted as below on the left.

\begin{array}{c|c}
\od{\odh{
\gG\Connn{
\od{\odd{\odh{\gG_1}}{\dD_1}{\gH_1}{\sysS}}
\od{\odd{\odh{\gG_n}}{\dD_n}{\gH_n}{\sysS}}
\quad&\quad
\od{\odh{\ods{\gG_1}{\dD_1}{\gH_1}{}\star \ods{\gG_1}{\dD_1}{\gH_1}{}}}
\end{array}

If $\gG=\star\in\set{\lpar,\ltens}$ we may write the derivations as above on the right.

\cC\Cons{\vldownsmash{\od{\odd{\odh{\gG}}{\dD}{\gH}{\sysS}}}}
\coloneqq
is well-defined
for any
context $\cC\conso$ and any derivation

A proof in $\sysS$ is a derivation in $\sysS$ whose premise
is $\unit$.

A graph $\gG$ is provable in $\sysS$ (denoted $\proves[\sysS]{\gG}$) iff there is a proof in $\sysS$ with conclusion $\gG$.

§.§ Equivalent Definitions of $\GS$

We here show that the formulation of the system $\GS$ provided in this paper is equivalent to one provided in [4, 5].
In particular, in the previous these papers the rule $\sur$ was not included in the system.
However, as shown in [5] this rule plays a crucial role in the proof that $\GS$ is a conservative extension of $\MLLx$
and in
[2] it is shown that this rule cannot be admissible in the proof systems operating on mixed graphs.

Moreover, we here give a weaker side condition on the $\prule$-rule with respect to the rules below:

\begin{equation}
\adjustbox{max width=.9\textwidth}{$\begin{array}{c|c}
\pdr \mbox{ in [5]}
\pdr \mbox{ in [4]}
\\\hline\\
\vlinf{\wpdr}{\star}{\nP\connn{\gM_1,\ldots, \gM_n}\lpar \gP\connn{\gN_1,\ldots, \gN_n}}{(\gM_1\lpar \gN_1)\ltens\cdots\ltens(\gM_n\lpar\gN_n)}
\vlinf{\wwpdr}{\dagger}{\nP\connn{\gM_1,\ldots, \gM_n}\lpar \gP\connn{\gN_1,\ldots, \gN_n}}{(\gM_1\lpar \gN_1)\ltens\cdots\ltens(\gM_n\lpar\gN_n)}
\\\\
\star\coloneqq\begin{array}{l}
\gP\notin\set{\lpar,\ltens} \mbox{ prime }
\mbox{$\gM_i\neq\unit$ for all $i\in\intset1n$}
\end{array}
\dagger\coloneqq\begin{array}{l}
\gP\notin\set{\lpar,\ltens} \mbox{ prime }
\mbox{$\gM_i\lpar\gN_i\neq\unit$ for all $i\in\intset1n$}
\end{array}
\end{array}$}
\end{equation}

In order to prove the equivalence between our system and the ones in [4, 5] we recall the following lemma allowing us to prove that in $\GS$ we can derive any graph of the shape $\gG\limp\gG$.

Let $\gM_1, \dots, \gM_n,\gN_1, \dots,\gN_n$ and $\gG$ be graphs
such that
Then there is a derivation

\od{
\odd{\odh{(\gM_1 \lpar \gN_1)\ltens \cdots\ltens(\gM_n\lpar \gN_n)}}{}
{\cneg\gG\connn{\gM_1, \ldots, \gM_n} \lpar \gG\connn{\gN_1, \ldots, \gN_n}}{\set{\sur,\pdr}}

By induction on the modular decomposition of $\gG$.

Thanks to this lemma, we can therefore prove the admissibility of the weaker

The following version of $\pdr$ with weaker side conditions
is admissible in $\GS$

\vlinf{\wpdr}{
\text{\scriptsize$\gP$ prime, $\gM_i\neq\unit$ for all $i\in\intset1n$}
}{\nP\connn{\gM_1,\ldots, \gM_n}\lpar \gP\connn{\gN_1,\ldots, \gN_n}}{(\gM_1\lpar \gN_1)\ltens\cdots\ltens(\gM_n\lpar\gN_n)}

Note that we may have $\gN_i=\unit$ for some $i\in\intset1n$.
Thus, if $\gN_i\neq\unit$ for all $i\in\intset1n$, then $\wpdr$ is an occurrence of $\pdr$.
Otherwise, w.l.o.g.,
$\gN_1=\unit$, thus
we have a derivation

\odiso{
\gM_1\ltens
\od{\odd{\odh{(\gM_2\lpar \gN_2)\ltens\cdots\ltens(\gM_n\lpar\gN_n)}}{}{
\nH\connn{\gM_2,\ldots, \gM_n}
\lpar
\gH\connn{\gN_2,\ldots, \gN_n}
\odn{\gM_1\ltens\nP\connn{\unit, \gM_2,\ldots, \gM_n}}{\sur}{\nP\connn{\gM_1, \gM_2,\ldots, \gM_n}}{} \lpar \gP\connn{\unit, \gN_2,\ldots, \gN_n}

Let $\gG$ be a graph.

\proves[\GS]\gG
\Leftrightarrow
\proves[\set{\aidr,\sdr,\sur,\wpdr}]\gG
\Leftrightarrow
\proves[\set{\aidr,\sdr,\wpdr}]\gG
\Leftrightarrow
\proves[\set{\aidr,\sdr,\wwpdr}]\gG

The first equivalence follows from <Ref>.
The other has been proved in [5].

§ ON RULES INTRODUCING A CONNECTIVE AT A TIME

A rule introducing only one connective (different from $\lpar$ and $\ltens$) at a time inevitably leads to the same problem observed in the literature of generalized multiplicative connectives [22, 32, 48, 6],
where initial coherence (i.e. the possibility of having only atomic axioms in a cut-free system, [11]) is ruled out because of the so-called packaging problem.

However, in this appendix we discuss the results about the system extending multiplicative linear logic with the rule $\conr$, that is, the system.

\MLLC \coloneqq\Set{\axrule,\lparr,\ltensr, \mixr,\conr[\con[\gP]] \mid\gP\in\primesign}
\quad\mbox{where}\quad
\vliiinf{\conr[\con[\gP]]}{}{
\vdash\Gamma_1, \ldots, \Gamma_n, \con[\gP]\connn{\fA_1, \ldots, \fA_n}
\vdash\Gamma_1, \fA_1
\qquad\cdots\qquad
\vdash\Gamma_n, \fA_n

We first observe that in the system does not satisfy anymore initial coherence;
e.g., the formula $\con[\Pfour]\connn{a,b,c,d}\limp \con[\Pfour]\connn{a,b,c,d}$ is not provable anymore.
However, the system still satisfies cut-elimination. The proof cut-elimination is straightforward by considering the following additional cut-elimination steps.

\begin{equation*}
\adjustbox{max width =\textwidth}{$
\begin{array}{c}
\vlderivation{
\vliin{\cutr}{}{
\vdash\Gamma_1,\ldots, \Gamma_n, \Delta_1, \ldots, \Delta_n
\vliiin{\conr}{}{
\vdash\Gamma_1,\ldots, \Gamma_n,\fP\connn{\fA_1, \ldots, \fA_n}
\vliiin{\conr}{}{
\vdash\Delta_1,\ldots, \Delta_n, \nfP\connn{\cneg\fA_1, \ldots, \cneg\fA_n}
\;\rightsquigarrow\;
\vlderivation{
\vliiiq{\mixr}{}{
\vdash\Gamma_1,\ldots, \Gamma_n, \Delta_1, \ldots, \Delta_n
\vliin{\cutr}{}{\vdash\Gamma_1,\Delta_1}{\vlhy{\vdash\Gamma_1,\fA_1}}{\vlhy{\vdash\Delta_1,\cneg\fA_1}}
\vlhy{\quad\cdots\quad}
\vliin{\cutr}{}{\vdash\Gamma_n,\Delta_n}{\vlhy{\vdash\Gamma_n,\cneg\fA_n}}{\vlhy{\vdash\Delta_n,\cneg\fA_n}}
\\\\
\vlderivation{
\vliin{\cutr}{}{
\vdash\Gamma_1,\ldots, \Gamma_n, \Delta_1, \ldots, \Delta_n,\nfP\connn{\fB_1, \ldots, \fB_n}
\vliiin{\dconr}{}{
\vdash\Gamma_1,\ldots, \Gamma_n,\nfP\connn{\fB_1, \ldots, \fB_n},\fP\connn{\fA_1, \ldots, \fA_n}
\vliiin{\conr}{}{
\vdash\Delta_1,\ldots, \Delta_n, \nfP\connn{\cneg\fA_1, \ldots, \cneg\fA_n}
\;\rightsquigarrow\;
\vlderivation{
\vliiin{\conr}{}{
\vdash\Gamma_1,\ldots, \Gamma_n, \Delta_1, \ldots, \Delta_n,\ncon\connn{\fB_1,\ldots,\fB_n}
\vliin{\cutr}{}{\vdash\Gamma_1,\Delta_1,\fB_1}{\vlhy{\vdash\Gamma_1,\fA_1,\fB_1}}{\vlhy{\vdash\Delta_1,\cneg\fA_1}}
\vlhy{\quad\cdots\quad}
\vliin{\cutr}{}{\vdash\Gamma_n,\Delta_n,\fB_n}{\vlhy{\vdash\Gamma_n,\cneg\fA_n,\fB_n}}{\vlhy{\vdash\Delta_n,\cneg\fA_n}}
\end{array}
\end{equation*}

Note that $\conr$ is derivable in $\PMLx$.

The rule $\conr$ is derivable in $\PMLx$.

If $\con=\lpar$, then $\conr$ is derivable using $\lparr$ and mix.
If $\con=\ltens$, then $\conr=\ltensr$.
Otherwise, we conclude by induction on the arity of $\con$ since we have a derivation

\vlderivation{
\vliin{\wdtr}{}{
\vdash\Gamma_1, \ldots, \Gamma_n, \con\connn{\fA_1,\ldots, \fA_n}
\vlhy{\vdash \Gamma_1, \fA_1}
\vlin{\unitor}{}{
\vdash\Gamma_2, \ldots, \Gamma_n, \con\connn{\funit,\fA_2,\ldots, \fA_n}
\vlpr{\dD'}{\IH}{\vdash\Gamma_2, \ldots, \Gamma_n, \fcC\connn{\fA_1,\ldots, \fA_n}}
%		\vlin{\unitor}{}{\vdash\Gamma_1, \ldots, \Gamma_n, \con\connn{\fA_1,\ldots, \fA_n} }{
%			\vlin{\lparr}{}{\vdash\Gamma_1, \ldots, \Gamma_n, \funit\lpar \con\connn{\fA_1,\ldots, \fA_n} }{
%				\vliq{(n-1)\times\unitor}{}{
%					\vdash\Gamma_1, \ldots, \Gamma_n, \funit, \con\connn{\fA_1,\ldots, \fA_n}
%				}{
%					\vliiin{\dconr}{}{
%						\vdash \Gamma_1,\ldots,\Gamma_n, \ncon\connn{\funit,\ldots, \funit} , \con\connn{\fA_1,\ldots, \fA_n}
%					}{
%						\vliin{\mixr}{}{\vdash \Gamma_1,\funit, \fA_1}{
%							\vlin{\urule}{}{\vdash \funit}{\vlhy{}}
%						}{
%							\vlhy{\vdash \Gamma_1, \fA_1}
%						}
%					}{\vlhy{\quad\cdots\quad}}{
%						\vliin{\mixr}{}{\vdash \Gamma_n,\funit, \fA_n}{
%							\vlin{\urule}{}{\vdash \funit}{\vlhy{}}
%						}{
%							\vlhy{\vdash \Gamma_n, \fA_n}
%						}
%					}
%				}
%			}
%		}

where $\dD'$ contains instances of $\conr$ introducing connectives whose arities are strictly smaller then the arity of $\con$.