A Complete Diagrammatic Calculus
for Boolean Satisfiability
Tao Gu
Robin Piedeleu
Fabio Zanasi
University College London
[ALL]Thanks to Guillaume Boisseau and Cole Comfort for helpful discussion on the completeness proof and  related work. RP and FZ acknowledge support from EPSRC grant EP/V002376/1.

We propose a calculus of string diagrams to reason about satisfiability of Boolean formulas, and prove it to be sound and complete. We then showcase our calculus in a few case studies. First, we consider SAT-solving. Second, we consider Horn clauses, which leads us to a new decision method for propositional logic programs equivalence under Herbrand model semantics.

String diagrams, Categorical semantics, Boolean algebra, Satisfiability, Logic programming

§ INTRODUCTION

In the 1970s, Cook and Levin proved independently <cit.> that a number of difficult problems reduce to that of determining the existence of a satisfying assignment to a given Boolean formula.  For this reason, in spite of its (suspected) theoretical intractability, and perhaps because of its surprising practical feasibility, the problem of Boolean satisfiability has acquired a central importance in logic and computer science.

This paper proposes a new perspective on the algebra of Boolean satisfiability, in the form of a sound and complete calculus of string diagrams.

At first glance, it may appear we already have a satisfactory algebraic treatment of Boolean satisfiability, dating back to the landmark works of George Boole in the 19th century <cit.>. Thanks to Boole, we know that classical propositional logic can be formulated as an algebraic theory, whose models are what we now call Boolean algebras. However, this standard treatment has a catch, which is the starting point of our work: the satisfiability of a propositional formula cannot be stated as a sentence in the algebraic theory of Boolean algebras. The reason is simple – algebraic theories only allow axioms as equations between terms with free variables (or, equivalently from the point of view of first-order classical provability, as equations in which every variable is universally quantified). On the other hand, a Boolean formula $f$ containing free variables $x_1,\dots, x_n$, is satisfiable if and only if
$\exists x_1\dots\exists x_n (f = 1)$,
which is outside of the algebraic realm. Call this formula SAT($f$); the algebraic theory of Boolean algebras is insufficiently expressive to encode SAT($f$) as a statement in the theory itself.

Of course, it is a perfectly well-formed first-order statement, so we could just use first-order logic to reason about SAT and derive the (un)satisfiability of particular instances.

However, we argue that a genuinely algebraic treatment of SAT is possible and preferable, provided that we move to a diagrammatic syntax. To this effect, we will introduce a calculus to compose systems of Boolean constraints expressed as string diagrams, and reason about them in a purely equational way.

Why would we need a diagrammatic syntax? As we have just shown, the algebraic theory of Boolean algebras is insufficiently expressive, thus we are looking for some other formal system that is more closely tailored to satisfiability. Existential quantification gives the problem a particularly relational flavour: SAT($f$) does not involve evaluating a Boolean function, but checking that there exists some assignment for which the function $f$ evaluates to true. This is a fundamentally relational, not functional constraint. And diagrammatic calculi are particularly well suited to express relational constraints, as demonstrated by the wealth of diagrammatic languages developed in recent years for different subcategories of relations (linear <cit.>, polyhedral <cit.>, affine <cit.>, piecewise-linear <cit.>). In this setting, string diagrams have the advantage of highlighting key structural features, such as dependencies and connectivity between different sub-terms/diagrams. Finally, another related way to think about string diagrams is as a multi-sorted algebraic syntax,  generalising standard algebraic syntax to the regular fragment of first-order logic, i.e. the fragment containing truth, conjunction, and existential quantification <cit.>.

In order to develop our approach, we take as semantic building blocks certain sets of satisfying assignments of Boolean formulas, which we organise into a symmetric monoidal category. We then devise a diagrammatic syntax for them generated by

\begin{equation*}
\tikzfig{generate-ar}
\end{equation*}

A diagram in this syntax is formed by composing any of the generators horizontally or vertically, connecting and crossing wires where needed. A dangling wire represents a free variable so that a diagram with $m$ wires on the left and $n$ wires on the right can be thought of as a Boolean formula in CNF with $m+n$ free variables. The intuition is that variables corresponding to wires on the left appear negatively in the associated formula, while those on the right appear positively. The correspondence between the syntax and the Boolean semantics is simple: each diagram is interpreted as the set of satisfying assignments of an associated formula.  It is helpful to give these formulas in CNF for the generators explicitly:

\begin{align*}
\copyy &\mapsto (\lnot x\lor y_1) \land (\lnot x\lor y_2)  \qquad &\discard\mapsto 1 \qquad\cocopy &\mapsto (\lnot x_1\lor y) \land (\lnot x_2\lor y)\qquad &\codiscard &\mapsto 1 \\
\coconj &\mapsto \lnot x\lor y_1\lor y_2\qquad &\unit\mapsto y\qquad  \conjj &\mapsto \lnot x_1\lor \lnot x_2\lor y\qquad &\counit &\mapsto \lnot x
\end{align*}

with the convention that $x$s correspond to left wires and $y$s to right wires.
Then, composing two diagrams in parallel (vertically) amounts to taking the conjunction of their associated formulas, while composing them in series (horizontally) requires existentially quantifying over the variable corresponding to the shared wire, effectively projecting it out.
Using these, we are able to encode arbitrary SAT instances – statements of the form $\exists x f$ for some CNF formula $f$ – as diagrams without any dangling wires.  For example, the SAT instance corresponding to $\exists x\exists y(\lnot x\lor y)\land (x\lor y)\land (x\lor \lnot y)\land (\lnot x\lor \lnot y)$ can be depicted as on the right.

The main technical result of this paper is a sound and complete equational theory for the intended semantics: any (in)equality that holds in the Boolean semantics, can be derived by equational reasoning at the level of the diagrams themselves. This theory, we argue, is the algebra of satisfiability.

Using our complete axiomatisation, we can derive the (un)satisfiability of any given SAT instance entirely diagrammatically, by applying local equational reasoning steps. For example, in a few steps, diagram above can be rewritten to $\tikzfig{wunit-wcounit}$, a diagram which represents the unsatisfiable formula $\exists x(\lnot x\land x)$.

We also take advantage of the fact that our syntax can represent Horn clauses to give a sound and complete encoding of propositional logic programs. We show how to represent definite logic programs diagrammatically and how their conventional semantics – their least Herbrand model – corresponds to the semantics of the associated diagram. Paired to the completeness result, this gives us a procedure to decide semantic equivalence of logic programs, by rewriting in the equational theory of our calculus — see e.g. Example <ref> below.

Synopsis. We introduce and motivate the semantic domain of interest in Section <ref>. We introduce the diagrammatic calculus in Section <ref>. We show how to use the calculus to reason about satisfiability in Section <ref>, and how to use it as a proof system for equivalence of logic programs in Section <ref>. We conclude with the proof of completeness in Section <ref>.

§ BOOLEAN FORMULAS, SATISFIABILITY AND MONOTONE RELATIONS

In this section we review the basics of Boolean formulas, and justify the introduction of monotone relations as a means to reason about their satisfiability.

We write $\Bool = \{0, 1\}$ for the two-element Boolean algebra, with the standard order $\{(0,0), (0,1), (1,1)\}$, and $\Bool^{op}$ for the same set with the opposite order. A Boolean formula is either $0$, $1$, a variable (from some given set of variables $x,y,\dots$), a conjunction of Boolean formulas $f_1\land f_2$, a disjunction of Boolean formulas $f_1\lor f_2$, or the negation of a Boolean formula $\lnot f$. Any Boolean formula with $n$ free variables admits a standard interpretation as a map $\Bool^n \to \Bool$ given by the usual Boolean semantics of conjunction, disjunction and negation (via their truth-tables). As is common practice, we will use the same notation to denote a Boolean formula $f$ and its interpretation $f\colon\Bool^n \to \Bool$.

We call literal a variable or the negation of a variable. We say that a formula is in conjunctive normal form (also known as clausal form) (CNF) when it is given as a conjunction of disjunctions of literals, e.g. $(\lnot x \lor y\lor z) \land (x\lor z \lor \lnot y)$. Each of the disjunctions of literals is called a clause. De Morgan duality guarantees that every Boolean formula admits a CNF formula with the same interpretation, i.e. that defines the same map $\Bool^n \to \Bool$. The equivalent formula in CNF can be obtained by pushing all the negations to the level of variables and distributing all disjunctions over conjunctions.

Given a Boolean formula $f: \Bool^n\to \Bool$, we call a satisfying assignment of $f$ any tuple of Booleans $(b_1, \dots, b_n)\in \Bool^n$ such that $f(b_1, \dots, b_n) = 1$. We say that a formula is satisfiable if it has at least one satisfying assignment. The satisfying assignments of a given formula $f$ with $n$ variables carve out a subset $[f=1] :=\{(b_1,\dots, b_n) : f(b_1,\dots, b_n) = 1\}$ of $\Bool^n$.

As mentioned in the introduction, satisfiability – the existence of a satisfying assignment for a given Boolean formula – is a relational constraint. Furthermore, relations tend to admit well-behaved diagrammatic calculi. For these two reasons, we turn to relations as our semantics.

The class of relations to consider is naturally suggested to us once we examine more closely the satisfying assignments of clauses, the fundamental building block of CNF formulas. Let $c_{m,n} = \lnot x_1\lor \dots \lor \lnot x_m\lor y_1\lor \dots \lor y_n$ be a clause, with $m$ negative literals and $n$ positive ones. Note the satisfying assignments of $c_{m,n}$ form a subset $[c_{m,n}=1]$ of $\Bool^m\times\Bool^n$ that is compatible with the order over $\Bool$: if $(a_1,\dots, a_m, b_1,\dots, b_n)$ is a satisfying assignment of $c_{m,n}$, any other assignment $(a_1',\dots, a_m', b_1',\dots, b_n')$ such that $a_i'\leq a_i$ and $b_j\leq b_j'$ for all $1\leq i\leq m$ and $1\leq j\leq n$, is also satisfying. In other words, $[c_{m,n}=1]$ is an upward-closed subset of $(\Bool^{op})^m\times \Bool^n$, where the order on the product of posets $X\times Y$ is given by $(x,y)\leq_{X\times Y} (x',y')$ iff $x\leq_X x'$ and $y\leq_Y y'$. For example, the clause $\lnot x\lor y_1\lor y_2$ has as satisfying assignments $(0,(0,0)), (1, (1,0)), (1,(0,1))$ and all tuples that are greater than these in $\Bool^{op}\times \Bool^2$. Another example: the set of satisfying assignments of $\lnot x \lor y$ is $\{(0,0), (0,1), (1,1)\}$ defines an upward-closed subset of $\Bool^{op}\times\Bool$ which we have already encountered as the order on $\Bool$ itself, i.e., $\{(x,y) \,|\, x\leq y\}$.

This monotonicity property of clauses and their sets of satisfying assignments suggests the following definition for the kind of relations that we wish to study.

A monotone relation $R:X\to Y$ between two posets $\lr{X, \leq_X}$ and $\lr{Y, \leq_Y}$ is a relation $R \subseteq X \times Y$ satisfying the following monotonicity condition: if $(x, y) \in R$, then for arbitrary $x' \in X$ and $y' \in Y$, $x' \leq x$ and $y \leq y'$ imply $(x', y') \in R$.

Monotone relations compose as expected: $R \relThen S \coloneqq \{ (x, z) \mid \exists y \text{ such that } (x, y) \in R, (y, z) \in S \}$. Also, the composition of monotone relations is monotone, so we can organise them into a category.

Posets together with monotone relations between them form a category, denoted as $\catBProf$. Moreover, $\catBProf$ equipped with the product of posets and the one-element poset $\lr{\{*\}, \{ (*, *) \}}$ forms a symmetric monoidal category

Note that we can turn a monotone function $f$ into the monotone relation $\{(x,y)\, |\, f(x)\leq y\}\subseteq X\times Y$, so that $\catBProf$ contains the category of monotone functions as a subcategory.

Having established their connection to satisfiability, we focus on monotone relations between tuples of Booleans, i.e. between products of the two-element Boolean algebra $\Bool$ (and its dual $\Bool^{op}$), as our primary semantic objects of interest. In the next two sections, we will develop a diagrammatic calculus axiomatising the full symmetric monoidal subcategory of $\catBProf$ spanned by finite Boolean algebras. Moreover, the calculus will shed further light on the relationship between monotonicity and satisfiability. At first glance, from the point of view of satisfiability, it looks like something is lost by restricting our semantics to monotone relations. However, the results of Sections <ref> and <ref> demonstrate that, perhaps surprisingly, this is not the case. We will come back to this specific point in Remark <ref>.

§ THE DIAGRAMMATIC CALCULUS

In this section we introduce $\catSata$ (SATisfiability Algebra), a diagrammatic calculus for monotone relations. It will consist of a syntax of string diagrams (Definition <ref>) and an inequational theory (Figure <ref>). The semantic interpretation will be given by a symmetric monoidal functor from the syntax category  to the category of monotone relations (Definition <ref>). We will later prove that the inequational theory is sound and complete for this interpretation.

We call $\catSyn$ the strict symmetric monoidal category freely obtained from a single generating object $1$ and the following generating morphisms, depicted as string diagrams <cit.>:

\begin{equation}\label{eq:catsyndef-generators}
\tikzfig{generate-ar}
\end{equation}

We write $\catSata$ for the category $\catSyn$ quotiented by

[Strictly speaking, since $\axBARel$ is an inequational theory, the result is a 2-category where morphisms are posets (thus poset-enriched categories). For simplicity we choose to present it as a category, and reason about the ordering on morphisms externally. The same strategy is applied to the poset-enriched category $\catBProf$ with ordering $\subseteq$. ]

the axioms of Figure <ref>. For a review of how to form this quotient and, more broadly, of the general methodology of presenting symmetric monoidal categories via (in)equational theories, we refer the reader to <cit.>, in particular Section 3 of that work.

We shall identify the monoidal product $1^{\tensor n}$ of $n$ copies of $1$ with the natural number $n$, and write $\tikzfig{id-morphism}$ for the identity morphism on $1$ and $\swap$ for the symmetry morphism on $1$. We depict the monoidal product $c\tensor d$ of two diagrams as their vertical juxtaposition, and the composition $c\then d$ as the horizontal concatenation of $c$ and $d$. We now describe the interpretation of string diagrams as monotone relations.

Let $\intBProf{\cdot} \colon \catSyn \to \catBProf$ to be the (lax) symmetric monoidal functor freely obtained by mapping the generating object $1$ to $\Bool$ and the generating morphisms of $\catSyn$ as follows:

\begin{align*}
\intBProf{\tikzfig{copy}} & = \{ (x, (y_1, y_2)) \mid x \leq y_i, ~\text{and}~ x, y_1, y_2 \in \Bool \}
& \quad &
\intBProf{\tikzfig{discard}}  \ = \ \{ (x, \bullet) \mid x \in \Bool \}
\\
%    & = \{ (x, (y_1, y_2) ) \mid x \leq y_1 \land y_2 ~\text{and}~ x, y_1, y_2 \in \setTwo{} \} \\
\intBProf{\tikzfig{cocopy}} & = \{ ((x_1, x_2), y) \mid x_i \leq y, ~\text{and}~ x_1, x_2, y \in \Bool \}      & \qquad &
\intBProf{\tikzfig{codiscard}}  \ = \ \{ (\bullet, x) \mid x \in \Bool \}
\\
\intBProf{\tikzfig{conj}} & = \{ ((x_1, x_2), y) \mid x_1 \land x_2 \leq y, ~\text{and}~ x_1, x_2, y \in \Bool \}
& \qquad &
\intBProf{\tikzfig{unit}} \ = \ \{ (\bullet, 1) \}
\\
\intBProf{\tikzfig{coconj}} & = \{ (x, (y_1, y_2)) \mid x \leq y_1 \lor y_2, ~\text{and}~ x, y_1, y_2 \in \Bool \}
& \qquad &
\intBProf{\tikzfig{counit}}  \ = \ \{ (0, \bullet) \}
%    \intBProf{\scalebox{0.8}{\tikzfig{cap}}} & = \{ (x_1, x_2) \mid x_2 \leq x_1, ~\text{and}~ x_1, x_2 \in \setTwo{} \} \\
%    \intBProf{\scalebox{0.8}{\tikzfig{cup}}} & = \{ (y_1, y_2) \mid y_1 \leq y_2, ~\text{and}~ y_1, y_2 \in \setTwo{} \}
\end{align*}

Note that, as $\intBProf{\cdot}$ is freely generated, $\intBProf{\tikzfig{id-morphism}} \coloneqq \{ (x, y) \mid x \leq y ~\text{and}~ x, y \in \Bool \}$, $\intUndirProf{c \then d} \coloneqq \intUndirProf{c} \relThen \intUndirProf{d}$, and $\intUndirProf{c \tensor d} \coloneqq \intUndirProf{c} \times \intUndirProf{d}$.

In general, the interpretation provided by $\intBProf{\cdot}$ is not faithful: distinct morphism of $\catSyn$ may be mapped to the same monotone relation. However, when we quotient the syntax by the inequational theory $\axBARel$ (Figure <ref>) the mapping $\catSata \to \catBProf$ we obtain from the quotiented syntax to the semantics is still a symmetric monoidal functor and is now faithful – this is what we mean by soundness (functoriality) and completeness (faithfulness) of $\axBARel$.

Degenerate bimonoid

Frobenius algebra

White-black and black-white bimonoids

The equational theory $\axBARel$

For any $c, d \in \catSynDef$, $c \leq_{\catSata} d$ if and only if $\intBProf{c} \subseteq \intBProf{d}$.

The proof will be given in Section <ref>. We now highlight some features of $\axBARel$. They will come handy when using it to study Boolean satisfiability and logic programming, in the next two sections.

* (A1)-(A4) state that $\copyy$ and $\discard$ form a commutative comonoid, while (A5)-(A8) states that $\cocopy$ and $\codiscard$ form a commutative monoid. In standard algebraic syntax, we can implicitly associate multiple applications of a monoid operation say, to the left, in order to avoid a flurry of parentheses, e.g. $a \lor b \lor c = (a \lor b) \lor c$. Thanks to laws (A1)-(A4), the same principle applies to an associative $2\to 1$ diagram of $\axBARel$. This justifies introducing generalised $n$-ary operations $\scalebox{0.8}{\tikzfig{n-ary-monoid}}$ as syntactic sugar. The same works for comonoids, by simply flipping the definitions as $\scalebox{0.8}{\tikzfig{n-ary-comonoid}}$.

* (B1)-(B10) state that $\conjj, \unit, \coconj, \counit$ forms a Frobenius algebra <cit.>.
A first important consequence is that this structure makes
$\catSata$ a compact closed category <cit.>, a category in which one can interpret fixed-points or iteration <cit.>.

Specifically, we have a cup $\tikzfig{cup}$ and cap $\tikzfig{cap}$ defined as $\tikzfig{cup-white-1}$ and $\tikzfig{cap-white-1}$ respectively, satisfying the `snake' equation $\scalebox{0.8}{\tikzfig{yanking-eq}}$. Note that axiom (A14) is defined with these as syntactic sugar.

Moreover, Frobenius algebras greatly reduce the mental load in keeping track of different ways of composing $\conjj, \unit, \coconj, \counit$, as they turn out to be equal. This simplification is more formally stated as the spider theorem — see e.g. <cit.>.

If $\conjj, \unit, \coconj, \counit$ form a commutative Frobenius structure, any connected morphism $m \to n$ made out of $\conjj, \unit, \coconj, \counit$, identities, symmetries, using composition and the monoidal product, is equal to the normal form spider-normal-form.

In the statement, the word connected refers to the diagram as a undirected graph: we assume there is at least one path made up of wires, between any two white nodes in the diagram.

In our axiomatic theory, we can simplify the normal form of Theorem <ref> even further to get rid of loops. Making crucial use of axiom (A14), we can derive $\tikzfig{not-special}$ (O).

Note it is unusual for a Frobenius algebra to satisfy (O) as those that have appeared in the literature satisfy a version of (O) with the rhs set to the identity (e.g. <cit.>) or to $\counit\;\unit$ (e.g. <cit.>).

Thanks to the spider theorem and equation (O), we can see any simply connected composition of white monoids and comonoids as a single node, whose only relevant structure is its number of dangling wires on the left and on the right. The normal form guarantees that we can unambiguously depict any such morphism $m\to n$ as a spider with $m$ wires on the left and $n$ on the right: $\tikzfig{spider}$.
With this syntactic sugar, the axioms of the Frobenius structure $\conjj, \unit, \coconj, \counit$ can be concisely expressed via the following spider fusion scheme:

\[\tikzfig{spider-fusion}\]

* The C block of axioms state that $(\copyy, \discard, \unit, \conjj)$ and $(\coconj, \counit, \codiscard, \cocopy)$ form two bimonoids. Semantically, these hold when the underlying poset is a lattice (has binary meets and joins). They also imply that $\catSata$ contains as a monoidal subcategory, the category of Boolean matrices with the direct sum as monoidal product.

* The D axioms present a number of adjunctions in the 2-categorical sense (or rather, Galois connections, because the 2-morphisms are simply inclusions). Two morphisms $f\colon X \to Y$ and $g\colon Y\to X$ are adjoint if $id_X \leq f\then g$ and $g\then f\leq id_Y$. We write this as $f\dashv g$ ($f$ left adjoint to $g$). The situation can be summarised by the following six adjunctions:

\begin{align*}
\conjj \dashv \copyy  \dashv \cocopy \dashv \coconj \qquad \qquad \qquad
\unit \dashv \discard \dashv \codiscard \dashv \counit
\end{align*}

The adjunctions $\copyy \dashv \cocopy$ and $\discard \dashv \codiscard$ give the defining inequations of cartesian bicategories <cit.>.

To understand where the other adjunctions come from, it is helpful to adopt a semantic perspective. For example, recall that  $\intBProf{\conjj} = \{((x_1,x_2),y) \mid x_1\land x_2 \leq y\}$ and $\intBProf{\copyy} = \{(x,(y_1,y_2)) \mid x\leq y_1, x\leq y_2\} = \{(x,(y_1,y_2)) \mid x\leq y_1 \land y_2\}$. Thus, one can see the adjunction $\conjj \dashv \copyy$ as arising from the duality between the two different ways of turning the monotone function $\land : \Bool^2\to \Bool$ into a monotone relation (by placing it on either side of the $\leq$ symbol in the corresponding set comprehension).

Semantically, they guarantee that the underlying poset $\Bool$ is a lattice, i.e., has binary meets and joins. Together with the Frobenius axioms (B9)-(B10), they imply that $\Bool$ is a complemented distributive lattice, in other words, a Boolean algebra.

Note that we did not aim for a minimal presentation of the theory. There are obvious redundancies: for example, axiom (C4) immediately implies (D4). Similarly, many equations of the B block can be derived from those of the D block and the corresponding properties of the black generators in the A block. We have included these redundancies in order to avoid burdening the reader with too many lemmas deriving equations that we will need often, and to highlight key algebraic structures that occur in related theories (e.g. bimonoids).

§ $\CATSATA$ AS THE ALGEBRA OF SATISFIABILITY

§.§ From diagrams to CNF formulas

The language we have introduced in the previous section can be seen as a diagrammatic notation to reason about Boolean formulas expressed in conjunctive normal form. As hinted at in the introduction, we can associate to every diagram a CNF formula, with the relational semantics of the diagram given by its set of satisfying assignments. The generators can be interpreted as follows:

\begin{align*}
\copyy &\mapsto (\lnot x \lor y_1) \land (\lnot x \lor y_2)  \qquad &\discard\mapsto 1 \qquad\cocopy &\mapsto (\lnot x_1 \lor y) \land (\lnot x_2 \lor y)\qquad &\codiscard \mapsto 1 \\
\coconj &\mapsto \lnot x \lor y_1 \lor y_2\qquad &\unit\mapsto y\qquad  \conjj &\mapsto \lnot x_1\lor \lnot x_2\lor y\qquad &\counit\mapsto \lnot x
\end{align*}

Note that an identity wire does not identify two variables $x=y$; rather, it represents the clause $\lnot x\lor y$.

The monoidal product is conjunction: if diagrams $d_1$ and $d_2$ correspond to some formulas $f_1$ and $f_2$ respectively, then their monoidal product corresponds to $f_1\land f_2$.

Composition is more subtle. As a plain identity wire represents the clause $\lnot x\lor y$, attaching two wires does not identity two variables, but merely adds this clause and existentially quantifies over $x$ and $y$. More precisely, given a formula $f$, let $\exists x f := f[x=1]\lor f[x=0]$, where $f[x=b]$ denotes $f$ in which we have replaced all occurrences of $x$ by the Boolean value $b$. Further assume, for simplicity, that we compose $\Diagbox{c}{m}{} \mapsto e$ and $ \Diagbox{d}{}{n}\mapsto f$ along a single wire: let $y$ be the variable that denotes the single wire in the codomain of $c$ and $x$ the single wire in the domain of $d$; then

One of the key observations is that the generalised white nodes introduced above, correspond to an arbitrary clause with $m$ negative literals and $n$ positive literals: $\tikzfig{spider} \quad \mapsto\quad  \lnot x_1\lor \cdots \lor \lnot x_m\lor y_1 \lor \cdots \lor y_n$.
Note that if we disallow the use of $\coconj$, we can only represent clauses with at most one positive literal, better known as Horn clauses. We will make extensive use of Horn clauses in the next section, to give a diagrammatic account of propositional logic programs.

We could have given an infinitary presentation of the same symmetric monoidal category with one generator for each clause containing $m$ negative literals and $n$ positive ones (keeping the same black generators).
We were able to give a presentation with a finite number of generators (and inequations) - with at most three wires - for the same reason that SAT can be reduced to $3$-SAT.

§.§ Picturing SAT

The payoff is that we can use the diagrammatic calculus to encode the satisfiability of arbitrary  Boolean formulas in a very natural way. Given a Boolean formula $f$ in CNF,  SAT($f$) can be depicted as a closed diagram (one of type $0\to 0$) of the form on the right, where the white nodes in the middle encode clauses and the black nodes take care of the variable management (copying and deleting) needed to connect variables to the clauses in which they appear, i.e. to the corresponding white nodes. The boxes are just permutations of the wires.

There are - up to equality - only two diagrams of type $0\to 0$, namely $\tikzfig{id-0}$ (the empty diagram) and $\tikzfig{wunit-wcounit}$, interpreted as the relations $\{\bullet\}$ and $\empset$, respectively.
Following the completeness of our equational theory, the soundness of our encoding of SAT implies that a formula $f$ is satisfiable iff the associated diagram is equal to $\tikzfig{id-0}$, as stated in Theorem <ref> below.
Furthermore, using our equational theory, we can derive the (un)satisfiability of a SAT instance purely algebraically, justifying the claim that our diagrammatic calculus captures the algebra of satisfiability.

Let us describe the encoding of SAT($f$) in more detail. Another way to understand the diagram above is as two relations that represent the negative and positive occurrences of variables - given by the black nodes on the left and on the right respectively - in each clauses - given by the white nodes at the center. We can encode these two incidence relations as Boolean matrices: given a CNF formula $f$ with $n$ free variables and $k$ clauses (both arbitrarily ordered), let $N(f)$ be the $k\times n$ Boolean matrix with $N(f)_{i,j} = 1$ iff $\lnot x_i$ appears in the $j$-th clauses of $f$, and $P(f)$ be the $n \times k$ Boolean matrix where $P(f)_{j,i} = 1$ iff $x_i$ appears in the $j$-th clauses of $f$.

In other words, $N(f)$ encodes negative occurrences of variables, and $P(f)$ their positive occurrences in each clause.

We use the standard diagrammatic representation of matrices using a commutative bimonoid to define diagrams for $N(f)$ and $P(f)$. For a review of this, we refer the reader to <cit.>.

We use below the same names for the associated diagrams: $N(f)$ denotes the corresponding matrix encoded using $\copyy, \discard, \unit, \conjj$, and $P(f)^T$ the transpose of $P(f)$ encoded using $\coconj, \counit, \codiscard, \cocopy$.

A CNF formula $f$ is satisfiable if and only if
$\ \scalebox{0.7}{\tikzfig{sat-encoding}} \; = \; \tikzfig{id-0}$.

Consider $f = (\lnot x\lor y)\land (x\lor y)\land (x\lor \lnot y)\land (\lnot x\lor \lnot y)$.

Following the notation in Theorem <ref>, let $N(f) = \tikzfig{cnf-eg-neg}$ where the left wires represent the negative occurrences of $x$ and $y$ respectively, from top to bottom, and the right wires represent the four clauses $(\lnot x\lor y), (x\lor y), (x\lor \lnot y)$, and  $(\lnot x\lor \lnot y)$ also from top to bottom. Similarly, let $P(f)^T = \tikzfig{cnf-eg-pos}$ encode all positive occurrences of $x$ and $y$ (right wires) into each of the clauses (left wires). Therefore SAT($f$) can be encoded diagrammatically as

\[\tikzfig{sat-instance-ex-2}\]

As we will explain below, in Subsection <ref>, the central inequality can be seen as an instance of resolution.

$(\lnot x\lor y)\land (x\lor \lnot y)$. Here, we have two variables that appear precisely once as negative and positive literals in two clauses:

$P(f)$ and $N(f)$ are both equal to a single identity wire.

This gives the following, which we can prove is satisfiable equationally:

\[\tikzfig{sat-instance-ex-1}\]

Inequalities can be used to prove that a formula is (un)satisfiable more efficiently. As we have explained above, there are - up to equality - only two diagrams of type $0 \to 0$, namely  $\tikzfig{wunit-wcounit} \leq \tikzfig{id-0}$. Thus, if $d(f) \leq \tikzfig{wunit-wcounit}$ for some formula $f$, we can strengthen this inequality to an equality and conclude that $f$ is unsatisfiable. Similarly, if we can show that $\tikzfig{id-0} \leq d(f)$ then $d(f)=\tikzfig{id-0}$ so $f$ is satisfiable.

It is helpful at this point to pause the development in order to examine the relationship between monotonicity and satisfiability. As we have already pointed out, at first glance, it appears that restricting ourselves to monotone relations is insufficient to study satisfiability. Indeed, monotone formulas (i.e. those which do not use negation) are always satisfiable. Correspondingly, at the level of the diagrammatic syntax, we do not have access to a primitive negation operation, which non-monotonic. As a result, we can never explicitly enforce that a variable is the negation of another. So how can we encode SAT without negation? The key idea is that we do have a restricted form of negation, which corresponds to changing the direction of wires, using the cups and caps.

Even though the diagrammatic translation is straightforward, there first appears to be a mismatch between a given CNF formula and the semantics of the diagram representing a SAT instance. A variable appearing as a positive and negative literal in a given formula $f$, is depicted as two wires – one for its positive occurrences and one for its negative occurrences.

When we wish to existentially quantify over a variable of a SAT instance, we simply trace out the corresponding two wires, connecting them.
In the relational semantics, the resulting loop joining the two wires represents

the additional clause $\lnot y\lor x$, where $y$ always appear positively in other clauses, and $x$ always appears negatively. This leaves the possibility of setting both variables to $0$, which satisfies $\lnot y\lor x$ but does not match the intuition that these two variables should behave like negated version of each other. However, the assignment $y=0, x=0$ does not affect the satisfiability of the overall diagram representing the corresponding SAT instance[In light of Theorem <ref>, we say that a closed diagram $d$ is satisfiable when $\intBProf{d} = \{\bullet\}$.]. Indeed, an issue can only arise if the assignment $y=0, x=0$ is required to make the diagram satisfiable. But this can never be the case because $y$ always appears positively in any clause other than $\lnot y\lor x$. This implies that the satisfiability of the clauses in which $y$ appears will only depend on the other variables and therefore leave the overall satisfiability of the diagram unaffected.

§.§ SAT-solving, diagrammatically?

Now that we know how to represent SAT instances in our diagrammatic language, it is useful to give meaning to the axioms in the light of this interpretation. First, the (co)associativity, (co)unitality and (co)commutativity of the various (co)monoids are equivalent to the associativity, unitality and commutativity of $\land$ and $\lor$ in propositional logic. The loop removal axiom from Fig. <ref> admits a natural interpretation in terms of satisfiability: if $\exists x (C\lor x\lor \lnot x)$ for some clause $C$, we can always satisfy $x\lor \lnot x$ and therefore we can remove constraint imposed by the whole clause $C\lor x\lor \lnot x$, regardless of the assignment of values to the other variables appearing in $C$. This axiom allows us to remove this kind of redundant constraints.

That the white nodes form a Frobenius algebra is more interesting: it stems from the fact that $\exists x.(C\lor x)\land (D\lor \lnot x)$ allows us to deduce the clause $C\lor D$, and is thus the diagrammatic translation of the resolution rule <cit.> in classical propositional logic!

Resolution has come to occupy a central role in SAT-solving as modern SAT-solvers can be thought of as resolution proof systems. It is well-known that solvers based on a variant of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm <cit.> implement a form of tree-like resolution, while those that are augmented with clause learning (e.g. CDCL) correspond to more general forms of resolution proofs, that allow for the reuse of learned clauses <cit.>.

Tree-like resolution proofs can be easily interpreted diagrammatically. Recall from our interpretation of SAT instances that clauses are simply white nodes whose left (resp. right) wires encode negative (resp. positive) literals. Thus, if we have two clauses $C\lor x$ and $\lnot x \lor D$, the corresponding diagram will contain a subdiagram equal to the leftmost one in (<ref>) below. The black nodes in the subdiagram represent the fact that $x$ might also appear (negatively or positively) in other clauses.
From this, resolution allows us to deduce $C\lor D$; tree-like resolution proofs further impose that, if we apply a deduction step, we do not use the original clauses $C\lor x$ and $\lnot x \lor D$ again. This has a simple diagrammatic counterpart—we can apply axiom (D6) to connect the two white nodes corresponding to the two clauses in premise of a resolution step directly, effectively replacing them with a single node that represents the learned clause:

\begin{equation}\label{eq:satexample}
\scalebox{0.8}{\tikzfig{tree-resolution}}
\end{equation}

The remaining wire for other uses of $x$ is unaffected. We have already used the same idea in Example <ref> above, in order to resolve the subdiagrams corresponding to the clauses $\lnot x\lor y$ and $x\lor y$.

General resolution – where we are allowed to keep the two clauses in the premise of the rule – also has a diagrammatic counterpart. In fact, it is implemented as a sequence of equalities (instead of the inequality we have used above to interpret tree-like resolution), reflecting the fact that the process does not forget any information. The idea is to first copy the two clauses $C\lor x$ and $\lnot x \lor D$ to leave them available for any further resolution with other clauses that use the variable $x$. We illustrate this process with two clauses (containing only three literals for simplicity this time) below:

\[\scalebox{0.8}{\tikzfig{general-resolution}}\]

In the resulting diagram, the quaternary white node represents the clause $C\lor D$, while the other two represent the original clauses $C$ and $D$.

§ $\CATSATA$ AS A PROOF SYSTEM FOR LOGIC PROGRAMMING

In this section we turn to logic programming.

$\catSata$ allows us to compute the usual semantics of propositional definite logic programs via diagrammatic equational reasoning (Theorem <ref>).

More importantly, we obtain a decidable, purely equational procedure to decide the equivalence of program, by proving the equivalence of their representing diagrams in $\catSata$ (Theorem <ref>).

First we briefly recall the basics of definite logic programming, and refer the readers to <cit.> for details.

Logic programming is a programming paradigm which reduces computation to proof search in formal logic. It is widely used in knowledge representation <cit.>, database theory <cit.>, constraint solving <cit.>. We focus on the simplest yet prototype class of logic programs, called propositional definite logic programs, formally defined as follows. We fix some finite set of atoms $\At = \{ a_1, \dots, a_k \}$. A Horn clause $\clauseD$ is a formula of the form $b_1, \dots, b_k \to a$, where $a, b_1, \dots, b_k \in \At$ and $b_1 \dots, b_k$ are distinct. Here the atom $a$ and the set $\{ b_1, \dots, b_k \}$ are called the head ($\head(\clauseD)$) and the body  ($\body(\clauseD)$) of the clause, respectively.

If a clause has an empty body, then it is also called a fact.

A propositional definite logic program (or simply logic program) is a finite set of Horn clauses based on $\At$.

Intuitively, a clause $b_1, \dots, b_k \to a$ reads `if $b_1, \dots, b_k$ hold, then $a$ also holds', which gives the intuitive meaning of a program $\progL$ to be the set of all atoms that are deducible from $\progL$ in finitely many steps.

This is formally defined as the least Herbrand
model semantics.

An interpretation $\intI$ over $\At$ is an assignment $\intI \colon \At \to \Bool$.

For simplicity, we will also write an interpretation $\intI$ over $\At$ as a subset $\{ a \in \At \mid \intI(a) = 1 \}$.

A logic program $\progL$ defines an immediate consequence operator $\imCnsqOp{\progL} \colon \Bool^{\At} \to \Bool^{\At}$ such that, given an interpretation $\intI$,

\[
\imCnsqOp{\progL}(\intI)(a) =
\begin{cases}
1 & \text{there exists $\progL$-clause}~ b_1, \dots, b_k \to a ~\text{such that}~ \intI(b_1) = \cdots = \intI(b_k) = 1 \\
0 & \text{otherwise}
\end{cases}
\]

The Herbrand model (denoted as $\leastHMod{\progL}$) is then the least fixed point of $\imCnsqOp{\progL}$. Such least fixed point always exists because $\Bool^\At$ carries a complete lattice structure, and $\imCnsqOp{\progL}$ is monotone on it.

We use the following notation: $\land$ and $\lor$ are defined pointwise on $\At$, $\funcOne$ and $\funcZero$ are the constant functions mapping arbitrary $a \in \At$ to $1$ and $0$, respectively.

From a deductive perspective, a logic program $\progL$ can be viewed as a black box: it takes a set of atoms $A$ as input, and outputs the set of atoms that are deducible from $A$ using $\progL$. This is formalised as the consequence operator $\cnsqOp{\progL} \colon \Bool^\At \to \Bool^\At$ of program $\progL$, such that
$\cnsqOp{\progL}(A)$ is the least Herbrand model of the program $\progL \cup \{ \to a \mid a \in A \}$. In particular, $\cnsqOp{\progL}(\empset)$ is exactly $\leastHMod{\progL}$.

Consider the program $\progP = \{ \to a; b \to d; c \to d; c,d \to b \}$ over $\At = \{ a, b, c, d \}$.

Its least Herbrand model $\leastHMod{\progP}$ is $\{ a \}$.
The immediate consequence operator $\imCnsqOp{\progP}$ maps, for instance, $\{ c \}$ to $\{ a, d \}$.

The consequence operator $\cnsqOp{\progP}$ maps, for instance, $\{ c \}$ to $\{ a, b, c, d \}$.

We will represent (immediate) consequence operators of logic programs via our diagrammatic language.

Immediate consequence operators have been studied from a string diagram perspective in <cit.>. Compared with (<ref>) below, there each clause is represented by a box, while our diagrammatic language enables us to `open the boxes' by representing a definite clause as $\tikzfig{conj-k}$.

The key observation is the intuitive reading of clause $b_1, \dots, b_k \to a$ as $b_1\land \dots \land b_k \leq a$, thus representable as the $\catSyn$-morphism $\tikzfig{k-conj}$.

The immediate consequence diagram $\imCnsqDiag{\progL}$ for program $\progL$ is an $n \to n$ morphism defined as follows, where the $i$-th input and output wires stands for atom $a_i$, for $i = 1,\dots, n$.

\begin{equation}\label{eq:im-conseq-diag}
\tikzfig{im-conseq}
\end{equation}

The two blue blocks $\tau_1$ and $\tau_3$ consist respectively of copiers $\tikzfig{copy}$ and cocopiers $\tikzfig{cocopy}$: $k_i$ and $\ell_i$ are the numbers of appearance of atom $a_i$ in all the bodies and heads of $\progL$-clauses, respectively.

The yellow block $\tau_2$ is the parallel composition of $\conjj$, where $q$ is the number of clauses in $\progL$, and for each clause $\clauseD_j$, $m_j$ is the size of $\body(\clauseD_j)$.

The grey blocks $\sigma_1$ and $\sigma_2$ consist of appropriately many $\swap$ that change the wire orders to match the domains and codomains of the blue and yellow blocks. In particular, the $i$-th input (resp. output) wire is connected to the $j$-th $\conjj$ if $a_i \in \body(\clauseD_j)$ (resp. $a_i = \head(\clauseD)$).

Based on this, we can compositionally represent the consequence operator $\imCnsqOp{\progL}$.

The consequence diagram for program $\progL$ is a $\catSyn$-morphism $\cnsqDiag{\progL} \colon n \to n$ defined on the right, where $\imCnsqDiag{\progL}$ is the immediate consequence diagram from Definition <ref>.

Note that the interpretation $\intBProf{\imCnsqDiag{\progL}}$ is not exactly the operator $\imCnsqOp{\progL}$: the former is a monotone relation while the latter is a monotone function. Nevertheless we say a monotone relation $R \subseteq X \times Y$ represents a monotone function $f \colon X \to Y$ if for arbitrary $x \in X$ and $y \in Y$, $(x, y) \in R$ if and only if $f(x) \leq y$.

Crucially, if monotone relations $R$ and $S$ represent monotone functions $f$ and $g$ respectively, then $f = g$ if and only if $R = S$.

The monotone relation $\intBProf{\imCnsqDiag{\progL}}$ (resp. $\intBProf{\cnsqDiag{\progL}}$) represents the operator $\imCnsqOp{\progL}$ (resp. $\cnsqOp{\progL}$).

Recall $\progP$ from Example <ref>.

$\imCnsqDiag{\progP}$ is given below left, coloured as in Definition <ref>.

Now we are ready to present the two main results for logic programs.

First, $\axBARel$ provides a diagrammatic calculus to compute $\cnsqOp{\progL}$, in particular to calculate the least Herbrand model as $\cnsqOp{\empset}$. One can represent an interpretation $\intI \in \setTwo^{\At}$ as a $\catSyn$-morphism $d^{\intI} \coloneqq d^{\intI}_1 \tensor \cdots \tensor d^{\intI}_n$ of type $0 \to n$, where each $d^\intI_i = \codiscard$ if $\intI(i) = 0$, and $d^\intI_i = \unit$ if $\intI(i) = 1$.

$\cnsqOp{\progL}(\intI)= \intJ$ if and only if $d
^\intI \then \cnsqDiag{\progL} = d^\intJ$.

Second, we can turn the problem of the equivalence of two logic programs into proving whether their consequence operator diagrams are equivalent. By Proposition <ref> and Theorem <ref>, we have:

Given two logic programs $\progL_1$ and $\progL_2$ on $\At$, $\cnsqOp{\progL_1} = \cnsqOp{\progL_2}$ if and only if $\cnsqDiag{\progL_1} = \cnsqDiag{\progL_2}$.

It is worth observing that, as we will see in Section <ref>, the completeness proof is essentially an algorithm that rewrites an arbitrary $\catSyn$-morphism into a normal form diagram (Definition <ref>). This means that the procedure described in Theorem <ref> to establish equivalence of logic programs in terms of consequence operators is in fact decidable.

Recall $\progP$ from Example <ref>, and let $\progQ = \{ \to a; a, b \to d; c \to b. \}$. We claim that $\progP$ and $\progQ$ are equivalent with respect to consequence operator.

One can show this by proving the equivalence of their consequence diagrams, namely $\cnsqDiag{\progP} = \cnsqDiag{\progQ}$:

\[
\scalebox{0.9}{\tikzfig{eg-cnsq-eq-1}}
\]

\[
\scalebox{0.9}{\tikzfig{eg-cnsq-eq-2}}
\]

It is helpful to point out that if we interpret $\catSyn$ in the category $\catRel$ of relations (via a functor $[-] \colon \catSyn \to \catRel$), then $\cnsqDiag{\progL}$ — an intuitive candidate to represent consequence operators — is not interpreted as $\{(\intI, \intJ) \mid \cnsqOp{\progL}(\intI) = \intJ \}$. In short, for the semantics to be correct, one has to define $[\copyy] = \{ (x, (x, x)) \mid x \in \Bool \}$ and $[\cocopy] = \{ ((x_1, x_2), y) \mid x_1, x_2, y \in \Bool, x_1 \lor x_2 = y \}$. But then the program $\progL = \{ a \to a \}$ has $\cnsqDiag{\progL} = \scalebox{0.7}{\tikzfig{vacuous-feedback}}$, and $[\cnsqDiag{\progL}] = \{ (x, y) \mid x, y \in \Bool, x \leq y \} \neq \{ (x, x) \mid x \in \Bool \} =  \cnsqOp{\progL}$.

§ SOUNDNESS AND COMPLETENESS

This section is devoted to the proof of Theorem <ref>, i.e. that the equational theory $\axBARel$ is a complete axiomatisation of monotone relations over (finite) Boolean algebras.

The `only if' direction (soundness) of Theorem <ref> is straightforward: we just need to show that each axiom is a valid semantic (in)equality. We take (C2) as an example, but will omit the verification of the other axioms:

\begin{align*}
%     \intBProf{\tikzfig{eg-soundness-1}} & = \{ ((x_1, x_2), (y_1, y_2)) \in \Bool^{4} \mid \exists z \in \Bool: x_1 \land x_2 \leq z, z \leq y_1 \land y_2 \} \\
%     & = \{ ((x_1, x_2), (y_1, y_2)) \in \Bool^{4} \mid x_1 \land x_2 \leq y_1 \land y_2 \} \\
\intBProf{\scalebox{0.8}{\tikzfig{eg-soundness-2}}} & = \{ ((x_1, x_2), (y_1, y_2)) \in \Bool^{4} \mid \exists z_1, z_2, z_3, z_4 \in \Bool: x_1 \leq z_1 \land z_2, x_2 \leq z_3 \land z_4, z_1 \land z_3 \leq y_1, z_2 \land z_4 \leq y_2 \} \\
& = \{ ((x_1, x_2), (y_1, y_2)) \in \Bool^{4} \mid \exists z_3, z_4 \in \Bool: x_2 \leq z_3 \land z_4, x_1 \land z_3 \leq y_1, x_1 \land z_4 \leq y_2 \} \\
& = \{ ((x_1, x_2), (y_1, y_2)) \in \Bool^{4} \mid \exists z_3, z_4 \in \Bool: x_1 \land x_2 \leq y_1, x_1 \land x_2 \leq y_2 \} \\
& = \{ ((x_1, x_2), (y_1, y_2)) \in \Bool^{4} \mid x_1 \land x_2 \leq y_1 \land y_2 \} = \intBProf{\scalebox{0.8}{\tikzfig{eg-soundness-1}}}
\end{align*}

We now focus on the `if' direction (completeness). Before the technical developments, we provide a roadmap of the proof. We first show that we can make two simplifying assumptions: (1) the completeness statement about inequalities/inclusions can be reduced to one that involves only equalities (Lemma <ref>); (2) We simplify the problem further by showing that we can restrict the proof of completeness to diagrams $m\to 0$ without loss of generality (Lemma <ref>).

To prove completeness for $m\to 0$ diagrams, we adopt a normal form argument that is common for the completeness proof of many diagrammatic calculi <cit.>.

In a nutshell, a normal form defines a certain syntactic representative for each semantic object in the image of the interpretation, and shows that if two diagrams have the same semantics, then they are both equal in $\axBARel$ to this syntactic representative.

The structure of the normal form argument is as follows.

* We give a procedure to rewrite any diagram into one in pre-normal form, using equations of $\axBARel$ (Lemma <ref>). Intuitively, pre-normal form diagrams represent sets of clauses of the form $\lnot x_1\lor \cdots \lor \lnot x_n$.

* Each downward closed subset is the set of satisfying assignment for a minimal set of such clauses (Lemma <ref>). The diagrammatic counterpart of this minimal set of clauses is our chosen normal form for each equivalence class of diagrams (Definition <ref>). We show that every diagram in pre-normal form is equal to one in normal form (Lemma <ref>).

* Finally, since every semantic object has a canonical diagrammatic representative – a normal form diagram – completeness follows from the fact that two diagrams having the same semantics have the same normal form (Proposition <ref>).

As explained above, completeness for equalities is enough to derive that for inequalities.

This follows from the next lemma, which essentially says that in lattices, inequalities can be defined using equalities and meets.

For diagrams $c, d$,
(i) if $\scalebox{0.8}{\tikzfig{plus-c-d}} = c$, then $c \leq d$ and (ii) if $\intBProf{c}\subseteq \intBProf{d}$ then  $\intBProf{\scalebox{0.8}{\tikzfig{plus-c-d}}}=\intBProf{c}$.

In addition, we can restrict the completeness proof to diagrams with codomain $0$. This is the consequence of axioms (B9)-(B10) which endow $\{ \coconj, \counit, \conjj, \unit \}$ with the structure of a Frobenius algebra and $\catSata$ with the structure of a compact closed category, allowing us to move wires from the left to the right and vice-versa.

For arbitrary natural numbers $m, n$, $\catSyn[m, n] \iso \catSyn[m+n, 0]$.

§.§ Pre-normal form

In this subsection, we show that every diagram is equivalent to one of pre-normal form, that is, which factorises as on the right. We then explore their close connection with certain Boolean clauses, a key tool in completeness proof.

Let us explain how to interpret the factorisation: each grey block represents a diagram which is formed only using the specified subset of generators (using both composition and monoidal product), possibly including some permutations of the wires.

The equational theory allows us to rewrite any diagram to pre-normal form.

Every diagram $m \to 0$ is equal to one of pre-normal form.

The first two blocks of pre-normal forms deserve special attention. We say that $d$ is a matrix diagram if it factorises as on the right.

In our semantics, matrix diagrams $m\to n$ denote relations that are the satisfying assignments of sets of Horn clauses, i.e. clauses  with at most one positive (unnegated) literal. For each Horn clause, the negated literals correspond to a subset of the left wires, while the only positive literal corresponds to the right wire to which they are connected. Intuitively,  matrix diagrams can be thought of simply as matrices with Boolean coefficients: each row encodes the negative literals of a Horn clause through its coefficients. An arbitrary $n\times m$ matrix $A$ can be represented by a matrix diagram with $m$ wires on the left and $n$ wires on the right—the left ports can be interpreted as the columns and the right ports as the rows of $A$ (cf. <cit.>). The $j$-th wire on the left is connected to the $i$-th wire on the right whenever $A_{ij}=1$; when $A_{ij}=0$ they remain disconnected. For example,
the matrix $A =
\begin{psmallmatrix}
0 & 1 & 1\\
0 & 1 & 0 \end{psmallmatrix}$ can be depicted as $\scalebox{0.8}{\tikzfig{matrix-ex}}$.

Conversely, given a diagram of this form, we can recover the corresponding matrix by looking at which ports are connected to which.
The equational theory $\axBARel$ is complete for the monoidal subcategory generated by $\copyy, \discard, \unit, \conjj$.

Let $c,d \colon m\to n$ be two diagrams formed only of the generators $\copyy, \discard, \unit, \conjj$. We have $\intBProf{c} = \intBProf{d}$ iff $c=d$ in $\axBARel$.

We can extract a unique matrix from a pre-normal form diagram, which we will call its representing matrix. Moreover,
Proposition <ref> allows us to simplify our reasoning in the proof of completeness: in light of this result, we will assume  – wherever it is convenient – that we can identify any two diagrams formed of $\copyy, \discard, \unit, \conjj$ that represent the same matrix. This often means that we can be as lax as necessary when identifying diagrams modulo the (co)associativity of $\copyy$ or $\conjj$ and the (co)unitality of $(\copyy, \discard)$ and $(\conjj, \unit)$. In particular, given a Boolean matrix $A$, we can define a unique (up to equality in $\axBARel$) pre-normal form diagram with representing matrix $A$.

Pre-normal forms are closely related to certain sets of Boolean clauses which we now introduce.

We fix a finite set of variables $\Var = \{ x_1, \dots, x_m \}$. By analogy with the corresponding terminology for Boolean formulas (cf. Section <ref>), we call a subset of $\Var$ a .

In the rest of this section, a  $\{x_{i_1}, \cdots, x_{i_k}\}$ is intended to represent the diagram $\tikzfig{cup-white-k}$ whose semantics is given by $\{x_{i_1}, \cdots, x_{i_k}\,|\, x_{i_1} \land \cdots \land x_{i_k} \leq 0\}$ which is equal to the set of satisfying assignments of $\lnot x_{i_1} \lor \cdots \lor \lnot x_{i_k}$[Strictly speaking, because all literals are negative, we should write $\{\lnot x_{i_1}, \cdots, \lnot x_{i_k}\}$ for the corresponding clause. However, to save the reader a flurry of negations, we will simply write it as the set $\{x_{i_1}, \cdots, x_{i_k}\}$.].

For conciseness, we sometimes write an assignment $\valS \colon \Var \to \Bool$ as

an element of $\Bool^m$, whose $i$-th element is $\valS(i+1)$, for $i = 0, \dots, m-1$. Given a  $\varphi=\{x_{i_1}, \cdots, x_{i_k}\}$, we say that an assignment $(b_1,\dots, b_m)$ satisfies $\varphi$ if $\lnot b_{i_1}\lor \cdots\lor \lnot b_{i_k} = 1$ (equivalently, if $b_{i_1}\land \cdots \land b_{i_k} = 0$). We say that it satisfies a set of  if it satisfies all  in the set simultaneously.

From pre-normal form to

Pre-normal form diagrams matter because one can derive a set of  from them, which is closely related with their semantics (Proposition <ref>).

Given some pre-normal form diagram $d \colon m \to 0$, we define $\sysIneq{}{d}$ to be the

set of  over $m$ variables as follows.

Each row $\rowR$ of the representing matrix $A$ of $d$ generates a  $\varphi$ such that $x_i \in \varphi$ if and only if $\rowR[i] = 1$, and $\sysIneq{}{d}$ is the set of all  generated by the rows of $A$.

The diagram $d$ and the set of  $\sysIneq{}{d}$ are semantically equivalent in the following sense.

Let $d \colon m \to 0$ be a pre-normal form diagram. Then $\intBProf{d}$ is exactly the set of all satisfying assignments of $\sysIneq{}{d}$, the le

set of  generated by $d$.

The diagram $d = \scalebox{0.8}{\tikzfig{eg-pre-NF-give-ineq-3}}$ is in pre-normal form and $\sysIneq{}{d} = \{\{x_1, x_2\}, \{x_1, x_3\}, \{\}\}$.

$\intBProf{d} = \empset$ is the set of all satisfying assignments of $\sysIneq{}{d}$.

From  to pre-normal form
Conversely, given a set of  $\Phi$ over $\Var$, we can define a diagram $\diag{\Phi} \colon m \to 0$ in pre-normal form.

Assume that $|\Phi| = n$, and we list the  in $\Phi$ using lexicographical order as $\varphi_1, \dots, \varphi_n$ (for instance, $\{ x_1, x_3 \}$ appears before $\{ x_2 \}$).

Then $\diag{\Phi}$ is defined as the pre-normal form diagram with representing $n\times m$ Boolean matrix $A$ given by $A_{ij} = 1$ precisely if $x_j \in \varphi_i$.

Again, $\Phi$ and $\diag{\Phi}$ are semantically equivalent in the following sense.

$\intBProf{\diag{\Phi}}$ is exactly the set of satisfying assignments of $\Phi$.

Let $\Var = \{ x_1, x_2, x_3 \}$, and consider the following two sets of :
$\Gamma = \{\{x_1\}, \{x_2, x_3\}\}$ and $\Phi = \{\{x_1\}, \{x_1, x_2\}, \{x_2, x_3\}\}$.

They have the same set of satisfying assignments $A = \{ 000, 010, 001 \}$; their associated pre-normal form diagrams are

$\diag{\Gamma} = \scalebox{0.7}{\tikzfig{eg-pre-NF-give-ineq-1}}$,

$\diag{\Phi} = \scalebox{0.7}{\tikzfig{eg-pre-NF-give-ineq-2}}$,

which verify $\intBProf{\diag{\Gamma}} = \intBProf{\diag{\Phi}} = A$.

Moreover, $\Phi$ contains the `redundant'  $\{x_1, x_2\}$ because the clause $\{x_1\}$ already implies that $\{x_1, x_2\}$ is satisfied (if $\lnot x_1 = 1$, then $\lnot x_1 \lor \lnot x_2 = 1$), while $\Gamma$ contains no such redundancies. Soon we shall see that $\Gamma$ is the smallest set of  whose set of satisfying assignments is $A$, and $\diag{\Gamma}$ is in normal form.

§.§ Normal form and completeness.

Recall that for completeness we want to select one representative diagram – in normal form –  for each semantic object.

We use sets of  as an intermediate step and choose such representative to be the minimal set of clauses among those with a given set of satisfying assignments: a set of  $\Phi$ is minimal if dropping any  from $\Phi$ returns a set $\Phi'$ whose set of satisfying assignments is a proper superset of those of $\Phi$. Minimal sets of  are unique, thus every given set of satisfying assignment for some set of  has a least set of .

If two minimal

sets of  $\Sigma$ and $\Gamma$ have the same satisfying assignments, then $\Sigma = \Gamma$.

A subset of $\Bool^{\Var}$ is downward closed if and only if it is the satisfying assignment of some set of  over $\Var$.

Lemmas <ref>-<ref> imply the existence of a unique minimal set of  for each semantic object.

For every downward closed subset $A$ of $\Bool^{\Var}$ there is a unique minimal

set of  whose solution set is $A$.

The normal form diagrams are defined as the diagrammatic counterpart of

minimal sets of .

Suppose $d \colon m \to 0$ is a pre-normal form diagram with representing matrix $A$.

We say $d$ is of normal form if there are no two distinct rows $i, j$ of $A$ such that $A_{ik} \leq A_{jk}$ for all $k = 1, \dots, m$.

Note that swapping two rows in the representing matrix $A$ of diagram $d$ does not change $\sysIneq{}{d}$ (the set of  generated by $d$), so what we really care about is normal form diagrams up to some permutation of the rows of their representing matrices.

Let $d$ and $e$ be two normal form diagrams with representing $n \times m$ matrices $A$ and $B$, respectively. $d$ and $e$ are equivalent up to commutativity if $A$ is $B$ with its rows permuted: for all $i \in \{ 1, \dots, n \}$, there exists some $j \in \{ 1, \dots, n \}$ such that $A_{i k} = B_{j k}$ for all $k = 1, \dots, m$, and vice versa.

Consider the pre-normal form diagrams above right.

$c_1$ is not of normal form because it represents the matrix $\begin{psmallmatrix}
1 & 1 & 0 \\
1 & 1 & 1
\end{psmallmatrix}$.

$c_2$ and $c_3$ are both of normal form, representing matrices
1 & 1 & 0\\
0 & 1 & 1 \end{psmallmatrix}$
0 & 1 & 1\\
1 & 1 & 0 \end{psmallmatrix}$
respectively, thus equivalent up to commutativity.

There is a 1-1 correspondence between the following three sets:

* downward closed subsets of $\Bool^m$;

* minimal sets of  over $\Var = \{ x_1, \dots, x_m \}$;

* normal form diagrams of type $m \to 0$, modulo equivalence up to commutativity.

The proposition above implies a stronger result plain completeness : $\axBARel$ is fully complete for the given semantics, as every monotone relation between tuples of Booleans is in the image of the interpretation functor $\intBProf{\cdot}$.

Having established the connection between semantic objects and normal form diagrams, we show that indeed every $\catSyn$-morphism is equal to one in normal form.

Crucially we need the following lemma, which allows us to remove redundant clauses from a diagram in pre-normal form to obtain one in normal form:

if some  $\phi$ is strictly larger than another $\psi$, then one can drop $\phi$ from $\Phi$ and the resulting set of  has the same set of satisfying assignments with the original $\Phi$.

For arbitrary natural numbers $m, n$,

Recall the two diagrams $\diag{\Gamma}$ and $\diag{\Phi}$ from Example <ref>, and we note that $\diag{\Phi}$ is in normal form while $\diag{\Gamma}$ is not. Yet we can apply Lemma <ref> (to the grey block) to rewrite $\diag{\Gamma}$ (on the lhs) into the normal form diagram $\diag{\Phi}$ (on the rhs):

Every diagram $d \colon m \to 0$ is equal to a diagram in normal form.

Finally we are ready to prove the completeness part of Theorem <ref>.

We start with the following completeness statement (involving only equalities), which follows from Proposition <ref> and Lemma <ref>.

For any diagrams $c, d \colon m \to n$, if $\intBProf{c} = \intBProf{d}$, then $c = d$.

We can then derive completeness from the following line of reasoning.

Proof of Theorem <ref>.
We assume that $\intBProf{c} \subseteq \intBProf{d}$. By Lemma <ref>(ii),
$\intBProf{\scalebox{0.8}{\tikzfig{plus-c-d}}} = \intBProf{c}$. By Lemma <ref>, this implies $\scalebox{0.8}{\tikzfig{plus-c-d}} = c$, thus $c \leq d$ according to Lemma <ref> (i).

§ CONCLUSION

An alternative approach to the problem of Boolean satisfiability is to consider the symmetric monoidal category of all relations between tuples of Booleans. A close cousin of this category – that of spans between finite sets with cardinality $2^n$ – was axiomatised in <cit.>. Adding a single axiom (to enforce transitivity of the order on $\Bool$) should be sufficient to obtain a complete axiomatisation of the corresponding category of relations. The resulting calculus would certainly be expressive enough to encode SAT instances and derive their (un)satisfiability equationally. However, the equational theory is more complex (reflecting the larger semantic domain), with two distinct Frobenius structures. Moreover, the monotonicity of our semantics, while seemingly limiting at first, allows us to topologise certain algebraic aspects of SAT: negation is represented as a change of the direction of wires, an essential feature of our calculus. These choices result in a tighter correspondence with formulas in CNF and a simpler equational theory, with close links to existing SAT-solving algorithms, as we have begun to investigate in Section <ref>. We hope to explore these connections further in future work, as well as the possibility of devising new heuristics for SAT-solving guided by the equational theory.

On the logic programming side,
the current paper extends work from <cit.>, in which two of the authors of the current paper propose a functorial semantics for logic programs.

Using the completeness result of the paper, we are able to go further to obtain a diagrammatic calculus to compute Herbrand semantics of logic programs, and show two programs are equivalent by proving the equivalence of two diagrams.

There are two main directions of further exploration.

The first is to extend the current framework to include more logical components, for example to consider logic programming admitting variables and/or negation.

The second is to invent a diagrammatic calculus for probabilistic and weighted logic programming.

§ REPRESENTING MONOTONE FUNCTIONS AS MONOTONE RELATIONS

Let us first restate the definition of a monotone relation representing a monotone function.

Let $\lr{X, \leq_X}, \lr{Y, \leq_Y}$ be two partially ordered sets. We say a monotone function $f \colon X \to Y$ is represented by a monotone relation $R \subseteq X \times Y$ if for arbitrary $x\in X$ and $y \in Y$, $(x, y) \in R$ if and only if $f(x) \leq y$.

If two monotone functions $f, g$ are represented by the same monotone relation $R$, then $f = g$.

We prove by contradiction. Suppose $f \neq g$ and they are represented by the same relation $R$, then there exists $x\in X$ such that $f(x) \neq g(x)$. Yet by the definition of $R$, both $(x, f(x))$ and $(x, g(x))$ are in $R$. We claim that this entails $f(x) = g(x)$.

Since $R$ represents $g$, $(x, f(x)) \in R$ implies that there exists $x' \in X$ such that $x \leq x'$ and $g(x') \leq f(x)$. Note that $g$ is monotone, so $g(x) \leq g(x') \leq f(x)$. Similarly, $R$ represents $f$ and $f$ is monotone imply that $f(x) \leq g(x)$. Now that $\lr{Y, \leq_Y}$ is a partial order means that $\leq_Y$ is antisymmetric, so $f(x) = g(x)$, which contradicts the assumption that $f(x)  \neq g(x)$. Therefore $f = g$.

The notion `being represented by' is closed under both sequential and parallel compositions:

* If $f \colon X \to Y$ and $g \colon Y \to Z$ are represented by $R\subseteq X \times Y$ and $S \subseteq Y \times Z$, respectively, then $f \then g \colon X \to Z$ is represented by $R \relThen S$.

* If $f \colon X \to Y$ and $g \colon U \to V$ are represented by $R \subseteq X \times Y$ and $S \subseteq U \times V$, respectively, then $f \times g \colon X \times U \to Y \times V$ is represented by $R \times S \subseteq (X \times U) \times (Y \times V)$.

* We show that for arbitrary $x \in X$ and $z\in Z$, $(x, z) \in R \relThen S$ if and only if $(f\then g) (x) \leq z$. For the `only if' direction, suppose $(x, z) \in R \relThen S$, then there exists $y \in Y$ such that $(x, y) \in R$ and $(y, z) \in S$. Since $R$ and $S$ represent $f$ and $g$ respectively, we know that $f(x) \leq y$ and $g(y) \leq z$, so by the monotonicity of $g$, $(f\then g)(x) = g(f(x)) \leq g(y) \leq z$ holds. For the `if' direction, suppose $(f\then g)(x) \leq z$, then $f(x) \leq f(x)$ implies that $(x, f(x)) \in R$. Also, $g(f(x)) \leq z$ implies that $(f(x), z) \in S$. So $(x, z) \in R\relThen S$.

* This is immediate from that both $f \times g$ and $R \times S$ are defined pointwise.

§ SOME USEFUL DIAGRAMMATIC (IN)EQUATIONS

We only prove the first two equations, and the other two follow from a similar proof by reflecting all the diagrams in the proof.

For the first equation,

\[
\tikzfig{unit-monoid-dif-color-1}
\]

For the second equation,

\[
\tikzfig{unit-monoid-dif-color-2}
\]

\begin{equation*}
\tikzfig{lem-loop-1}
\end{equation*}

Crucially we need (A14) for the second inequality.

\begin{equation}
\tikzfig{lem-loop-2}
\end{equation}

\begin{equation*}
\tikzfig{not-special}
\end{equation*}

The following distributivity equation holds:

\begin{equation}
\tikzfig{lem-conj-dist-disj}
\end{equation}

\begin{equation}
\tikzfig{proof-conj-dist-disj-2}
\end{equation}

The converse inequalities to (D2), (D5), and (D10) are derivable.

For (D2) we can derive the converse inequality as follows:
The other two are similar. For (D5) replace (D3) by (D7) and apply unitality (A6) of $\cocopy,\codiscard$ and counitality (A6) of $\copyy,\discard$. For (D10) replace (D3) by (D7) and apply unitality (A6) of $\cocopy,\codiscard$ and counitality (B2) of $\coconj,\counit$.

The following general bialgebra equation holds for all natural numbers $k, n$.

\begin{equation}
\label{eq:gen-bialg}
\tikzfig{gen-bialg}
\end{equation}

For readability, in the rest of the proof we will not use the dashed wires but instead use $\vdots$ and natural numbers to intuitively express that `there are $k$ duplicates of certain pattern'.

We prove by induction on $n$, and leave $k$ arbitrary.

When $n = 0$ and $n = 1$, we have

\begin{equation*}
\tikzfig{gen-bialg-proof-1}
\end{equation*}

When $n = 2$, we make an induction on $k$.

The base case for $k = 0, 1$ are exactly the same as the previous proof for $n = 0, 1$.

For $k = 2$, this is exactly the bialgebra axiom.

Now suppose it holds for $k \geq 2$, and we consider $k + 1$:

\begin{equation*}
\tikzfig{gen-bialg-proof-3}
\end{equation*}

We continue with the induction proof on $n$. Suppose equation (<ref>) holds for $n$, then for $n + 1$,

\begin{equation*}
\tikzfig{gen-bialg-proof-2}
\end{equation*}

The following bialgebra equation between $\coconj$ and $\cocopy$ (resp. $\conjj$ and $\copyy$) holds for arbitrary natural numbers $k, n$

\begin{equation}
\label{eq:gen-bialg-BW}
\tikzfig{gen-bialg-BW}
\end{equation}

The proof is the same as that for Proposition <ref>. Note that there only properties of $(\copyy, \cocopy)$ forms a bimonoid is used, which also holds for $(\copyy, \conjj)$ and $(\cocopy, \coconj)$, see the B and C axioms in Figure (<ref>).

§ OMITTED PROOFS IN SECTION <REF>

Theorem <ref>
Call $d(f)$ the leftmost diagram above. Computing its semantics, we get that

\[\intBProf{d(f)} = \{\bullet\} \quad \Leftrightarrow \quad \exists \mathbf{x} \exists \mathbf{y}\in \Bool^n \left( \mathbf{y}\leq \mathbf{x} \text{ and } N(f)\mathbf{x} \leq P(f)^T \mathbf{y} \right)\quad \Leftrightarrow  \quad \exists \mathbf{x} \in \Bool^n  \left(N(f)\mathbf{x} \leq P(f)^T \mathbf{x}\right)\]

If we use negation and disjunction for the Boolean algebra $\Bool^k$, the last condition can be written as $\exists \mathbf{x} \in \Bool^n  \left(\lnot N(f)\mathbf{x}\lor P(f)^T \mathbf{x}\right)$. This is a $k$-tuple of disjunctions that encode the same clauses as $f$ by construction. Therefore $\lnot N(f)\mathbf{x}\lor P(f)^T \mathbf{x}$ is satisfiable iff $f$ is and thus $\intBProf{d(f)} = \{\bullet\}$ iff $f$ is satisfiable. By completeness (Theorem <ref>), we conclude that $f$ is satisfiable iff $d(f) = \tikzfig{id-0}$.

§ OMITTED PROOFS IN SECTION <REF>

Proof of Proposition <ref>.
We show that for arbitrary interpretations $\intI, \intJ$ on $\At$, $(\intI, \intJ) \in \intBProf{\cnsqDiag{\progL}}$ if and only if $\cnsqOp{\progL}(\intI) \leq \intJ$.

\begin{equation}\label{eq:conseq-diag-rep-1}
\tikzfig{conseq-diag-rep-1}
\end{equation}

By the definition of the interpretation $\intBProf{\cdot}$, $(\intI, \intJ) \in \intBProf{\cnsqDiag{\progL}}$ if and only if there exist $\intK_i$ for $i = 1, \dots, 6$ such that:

$\intI, \intK_6 \leq \intK_1$;

$\intK_1 \leq \intK_2, \intJ$;

$(\intK_2, \intK_3) \in \intBProf{\imCnsqDiag{\progL}}$;

$\intK_3 \land \intK_4 \leq \funcZero$;

$\intK_5 \leq \intK_4$;

$\funcOne \leq \intK_5 \lor \intK_6$.

See (<ref>) for an illustration of these $\intK_i$.

We can simplify this condition by a sequence of equivalent conditions on $\intI, \intJ$ and those $\intK_i$:

$\intI, \intK_6 \leq \intK_2, \intJ$; $(\intK_2, \intK_3) \in \intBProf{\imCnsqDiag{\progL}}$; $\intK_3 \land \intK_4 \leq \funcZero$; $\intK_5 \leq \intK_4$; $\funcOne \leq \intK_5 \lor \intK_6$.

$\intI, \intK_6 \leq \intK_2, \intJ$; $(\intK_2, \intK_3) \in \intBProf{\imCnsqDiag{\progL}}$; $\intK_3 \leq \intK_6$.

$\intI, \intK_3 \leq \intK_2, \intJ$; $(\intK_2, \intK_3) \in \intBProf{\imCnsqDiag{\progL}}$.

$\intI, \intK_3 \leq \intK_2, \intJ$; $\imCnsqOp{\progL}(\intK_2) \leq \intK_3$.

$\intI, \imCnsqOp{\progL}(\intK_2) \leq \intK_2, \intJ$.

That is to say, $(\intI, \intJ) \in \intBProf{\cnsqDiag{\progL}}$ if and only if there exists $\intK$ such that $\intI, \imCnsqOp{\progL}(\intK) \leq \intK, \intJ$.

We claim that this is equivalent to that $\intJ \geq \lfp U. \intI \lor \imCnsqOp{\progL}(U)$, where $\lfp U. F(U)$ denotes the least fixed point of a monotone function $F$ on some complete lattice.

On one hand, if $\intJ \geq \lfp U. \intI \lor \imCnsqOp{\progL}(U)$, then let $\intK$ be $\lfp U. \intI \lor \imCnsqOp{\progL}(U)$. By the definition of fixed points, $\intI \lor \imCnsqOp{\progL}(\intK) = \intK$, we know that $\intI \leq \intK$ and $\imCnsqOp{\progL}(\intK) \leq \intK$. So $\intI, \imCnsqOp{\progL}(\intK) \leq \intJ$ as well.

On the other hand, suppose there exists $\intK$ such that $\intI, \imCnsqOp{\progL}(\intK) \leq \intK, \intJ$, then this is equivalent to $\intI \lor \imCnsqOp{\progL}(\intK) \leq \intK, \intJ$. $\intI \lor \imCnsqOp{\progL}(\intK) \leq \intK$ means that $\intK$ is a pre-fixed point for $\intI \lor \imCnsqOp{\progL}(-) \colon \setTwo^\At \to \setTwo^\At$, and by the Knaster-Tarski theorem, $\lfp U. \intI \lor \imCnsqOp{\progL}(U) \leq \intK$. Therefore, using the fact that $\imCnsqOp{\progL}$ is monotone, we have

\begin{equation}
\intJ \geq
\intI \lor \imCnsqOp{\progL}(\intK)
\geq \intI \lor \imCnsqOp{\progL}(\lfp U. \intI \lor \imCnsqOp{\progL}(U))
= \lfp U. \intI \lor \imCnsqOp{\progL}(U)
\end{equation}

Now note that $\lfp U. \intI \lor \imCnsqOp{\progL}(U)$ is exactly $\cnsqOp{\progL}(\intI)$ (Lemma <ref>), so we have $(\intI, \intJ) \in \intBProf{\cnsqDiag{\progL}}$ if and only if $\cnsqOp{\progL}(\intI) \leq \intJ$, which means that $\intBProf{\cnsqDiag{\progL}}$ represents the consequence operator $\cnsqOp{\progL}$.

Proof of Proposition <ref>.
We show that for arbitrary interpretations $\intI$, $\intJ$ on $\At$, $(\intI, \intJ) \in \intBProf{\imCnsqDiag{\progL}}$ if and only if $\imCnsqOp{\progL}(\intI) \leq \intJ$.

We start from the left-hand-side and use the notation from Definition <ref>,

\begin{align*}
& (\intI, \intJ) \in \intBProf{\imCnsqDiag{\progL}} \\
\iff & \exists \intK_1 \in \setTwo^{\ell_1}, \dots, \intK_n \in \setTwo^{\ell_n} \colon (\intI, (\intK_1, \dots, \intK_n)) \in \intBProf{\tau_1 \then \sigma_1 \then \tau_2 \then \sigma_2}, ( \intK_1, \dots, \intK_n), \intJ) \in \intBProf{\tau_3} \\
\iff & \exists \intK_1, \dots, \intK_n \colon (\intI, (\intK_1, \dots, \intK_n)) \in \intBProf{\tau_1 \then \sigma_1 \then \tau_2 \then \sigma_2}, \intK_i(j_i) \leq \intJ(i) \text{ for } \forall i = 1,\dots, n, j_i = 1, \dots, \ell_i \\
\iff & \text{for each $\progL$-clause } \clauseD \equiv a_{i_1}, \dots, a_{i_r} \to a_{i_s}, \intI(i_1) \land \cdots \land \intI(i_r) \leq \intJ(i_s) \\
\iff & \text{for each $\progL$-clause } \clauseD \equiv a_{i_1}, \dots, a_{i_r} \to a_{i_s}, \text{if } \intI(i_1) = \cdots = \intI(i_r) = 1, \text{then } \intJ(i_s) = 1 \\
\iff & \imCnsqOp{\progL}(\intI) \leq \intJ
%    \iff & \exists \intK_1, \dots, \intK_n \colon \text{for each clause } \clauseD \equiv b_{1}, \dots, b_{r} \to a,
\end{align*}

Then by Definition <ref>, this means that the monotone relation $\intBProf{\imCnsqDiag{\progL}}$ represents the immediate consequence operator $\imCnsqOp{\progL}$.

Proof of Theorem <ref>
By Theorem <ref>, $d
^\intI \then \cnsqDiag{\progL} = d^\intJ$ if and only if $\intBProf{d
^\intI \then \cnsqOp{\progL}} = \intBProf{d^\intJ}$. Since $\intBProf{d^\intI}$ and $\intBProf{\cnsqDiag{\progL}}$ represent $\intI$ and $\cnsqOp{\progL}$ respectively, $\intBProf{d^\intI \then \cnsqDiag{\progL}} = \intBProf{d^\intI} \relThen \intBProf{\cnsqDiag{\progL}}$ represents $\cnsqOp{\progL}(\intI)$, by the compositionality of representations <ref>. Then $\intBProf{d
^\intI \then \cnsqDiag{\progL}} = \intBProf{d^\intJ}$ is equivalent to $\cnsqOp{\progL}(\intI) = \intJ$.

Proof of Theorem <ref>
Note that $\intBProf{\cnsqDiag{\progP}}$ represents $\cnsqOp{\progP}$ (Proposition <ref>).

By Proposition <ref>, $\cnsqOp{\progP_1} = \cnsqOp{\progP_2}$ if and only if $\intBProf{\cnsqDiag{\progP_1}} = \intBProf{\cnsqDiag{\progP_2}}$. Then Theorem <ref> implies that this is equivalent to $\cnsqDiag{\progP_1} = \cnsqDiag{\progP_2}$.

$\cnsqOp{\progL}(\intI) = \lfp U. \intI \lor \imCnsqOp{\progL}(U)$.

By the definition of consequence operators in Section <ref>, $\cnsqOp{\progL}(\intI)$ is the least Herbrand model of the program $\progL \cup \{ \to a \mid a \in \At, \intI(a) = 1 \}$. So $\cnsqOp{\progL}(\intI) = \lfp U. \imCnsqOp{\progL \cup \intI} (U)$.

Note that for arbitrary programs $\progL_1$ and $\progL_2$ on $\At$, $\imCnsqOp{\progL_1 \cup \progL_2} = \imCnsqOp{\progL_1} \lor \imCnsqOp{\progL_2}$, because anything that is derivable in one step from $\intI$ using the union program $\progL_1 \cup \progL_2$ is either derivable via $\progL_1$ or derivable via $\progL_2$. Therefore $\lfp U. \imCnsqOp{\progL \cup \intI} (U) = \lfp U. \imCnsqOp{\progL}(U) \lor \imCnsqOp{\progP_{\intI}}(U)$, where $\progP_{\intI}$ is the program $\{ \to a \mid a \in \At, \intI(a) = 1 \}$.

Since the program $\progP_{\intI}$ consists solely of facts, $\imCnsqOp{\progP_{\intI}}$ maps any interpretation $\intJ$ to $\intI$, so $\cnsqOp{\progL}(\intI) = \lfp U. \imCnsqOp{\progL}(U) \lor \imCnsqOp{\progP_{\intI}}(U) = \lfp. \intI \lor \imCnsqOp{\progL}(U)$.

§ APPENDIX OF SECTION <REF>

§.§ Simplifying assumptions

Proof of Lemma <ref>
For (i), assume that $c= \tikzfig{plus-c-d}$. We have

\[
\tikzfig{syn-plus-leq-1}
\]

The last step uses the fact that $\tikzfig{syn-plus-leq-2} \leq \discard$ for all diagrams $f \colon m \to n$

which can proved via induction on the structure of $f$: the inductive cases are trivial and the base cases are given by axioms (A10) for $\cocopy$, (A12) for $\codiscard$, (A2)-(A3) for $\copyy$, trivial for $\discard$, (C3) for $\conjj$, (C4) for $\unit$, (A10) followed by (D10) for $\coconj$, (D8) followed by (C4) for $\counit$.

For (ii), assume that $\intBProf{c} \subseteq \intBProf{d}$. According to the semantics of $\copyy$ and $\cocopy$,
$\intBProf{\tikzfig{plus-c-d}} = \{ (x, y) \mid \exists x_1, x_2, y_1, y_2 \colon (x_1, y_1) \in \intBProf{c}, (x_2, y_2) \in \intBProf{d}, x\leq x_i, y_i \leq y, i = 1, 2 \} = \intBProf{c} \cap \intBProf{d} = \intBProf{c}$.

Proof of Lemma <ref>.

Towards the isomorphism, we define two functions $p \colon \catSyn[m, n] \to \catSyn[m+n, 0]$ and $q \colon \catSyn[m+n, 0] \to \catSyn[m, n]$, and prove that they are inverses to each other.

Given arbitrary $d \colon m \to n$ and $e \colon m+n \to 0$, we define $p(d)$ to be $\tikzfig{func-bijec-1}$, and $q(e)$ to be $\tikzfig{func-bijec-2}$.

Then one can show that $q \after p$ and $p \after q$ are identity functions, using the compact closed structure:

\begin{align*}
(q \after p) (d) & = q \left( \tikzfig{func-bijec-1} \right)
= \tikzfig{func-bijec-3}
= \tikzfig{func-bijec-4} \\
(p \after q) (e) & = p \left( \tikzfig{func-bijec-2} \right)
= \tikzfig{func-bijec-5}
= \tikzfig{func-bijec-6}
\end{align*}

This shows that $p$ and $q$ witness the bijection between $\catSyn[m, n]$ and $\catSyn[m+n, 0]$.

§.§ Matrices, diagrammatically

Our syntax contains a diagrammatic counterpart of Boolean matrices, about which we need to prove a few technical lemmas.

We say that $d$ is a matrix diagram if it factorises as follows:

\begin{equation}
\tikzfig{matrix-diagram}
\end{equation}

Matrix diagrams $m\to n$ denote relations that are the satisfying assignments of sets of Horn clauses, i.e. clauses  with at most one positive (unnegated) literal. For each Horn clause, the negated literals correspond to a subset of the left wires, while the only positive literal corresponds to the right wire to which they are connected. For this reason,  matrix diagrams can also be thought of simply as matrices with Boolean coefficients: each row encodes the negative literals of a Horn clause through its coefficients. An arbitrary $n\times m$ matrix $A$ can be represented by a matrix diagram with $m$ wires on the left and $n$ wires on the right—the left ports can be interpreted as the columns and the right ports as the rows of $A$. The $j$-th wire on the left is connected to the $i$-th wire on the right whenever $A_{ij}=1$; when $A_{ij}=0$ they remain disconnected. For example,

\[\text{the Boolean matrix } A =
\begin{pmatrix}
0 & 1 & 1\\
0 & 1 & 0
\end{pmatrix} \text{ can be depicted as } \tikzfig{matrix-ex}\]

Conversely, given a diagram of this form, we can recover the corresponding matrix by looking at which ports are connected to which.

A canonical matrix diagram $d \colon m \to n$ is a diagram of the following form:

\begin{equation}
\tikzfig{mat-diag-canonical-1}
\end{equation}

where each $\matEntry{i}{j}$ is either $\tikzfig{id-morphism}$ or $\tikzfig{disconnect}$, for $i = 0, \dots, m-1$ and $j = 0, \dots, n-1$; $\sigma$ contains suitably many $\swap$ that move the $j$-th output wire of the $i$-th $\copyy$ to the $i$-th input wire of the $j$-th $\conjj$.

The equational theory $\axBARel$ is complete for the monoidal subcategory generated by $\copyy, \discard, \unit, \conjj$.

Let $c,d \colon m\to n$ be two diagrams formed only of the generators $\copyy, \discard, \unit, \conjj$. We have $\intBProf{c} = \intBProf{d}$ iff $c=d$ in $\axBARel$.

The symmetric monoidal category of matrices with Boolean coefficients and the direct sum as monoidal product has a well-known complete axiomatisation: the theory of a commutative and idempotent bimonoid. This result can be found in <cit.>: therein the third author of this paper gives a complete axiomatisation of the symmetric monoidal category of matrices over a principal ideal domain (again with the direct sum as monoidal product). However the proof in <cit.> does not make any use of additive inverses and can be adapted without changes to the case of an arbitrary semiring, like the Booleans.

In $\axBARel$ the axioms defining a commutative and idempotent bimonoid are given in Fig. <ref> by equations (A1)-(A13). Note however that we care about matrices formed using $\copyy, \discard, \unit, \conjj$ here, so we need to check that the same equations hold with $\cocopy$ replaced by $\conjj$ and $\codiscard$ replaced by $\unit$. For this, we only need to show that we can strengthen (D2) to an equality (for idempotency). The converse inequality can be derived as follows:

\[\tikzfig{bcomult-wmult-equal-id}\]

This shows that the symmetric monoidal subcategory of $\catSata$ generated by $\copyy, \discard, \unit, \conjj$ embeds faithfully into the symmetric monoidal category of Boolean matrices.

The desired completeness result follows because the symmetric monoidal category of Boolean matrices embeds faithfully in our target category of monotone relations and that $\intBProf{\cdot}$ (or rather, the restriction of $\intBProf{\cdot}$ to the symmetric monoidal subcategory generated by $\copyy, \discard, \unit, \conjj$) factors through this embedding. To see this, notice that an $n\times m$ Boolean matrix $A$ defines a monotone function $f\colon \Bool^m\to \Bool^n$ whose $j$-th component is given by $f_j(x_1,\dots,x_m) =  x_{j_1}\land \cdots \land  x_{j_k}$ where $\{j_1,\dots, j_k\}$ is the set of indices in the $j$-th row of $A$ which are equal to $1$. Clearly, any two matrices that define the same monotone function are equal. In turn, we can embed monotone functions faithfully into monotone relations, as explained in Proposition <ref>.

Any diagram formed only of the generators $\copyy, \discard, \unit, \conjj$ is equal to a canonical matrix diagram.

The following matrix diagram is equivalent to a canonical matrix diagram on the right hand side:

\begin{equation}
\tikzfig{mat-diag-canonical-eg-3}
\end{equation}

In particular, the grey diagram is the $\sigma$ in Definition <ref>; $\matEntry{2}{1} = \matEntry{1}{3} = \matEntry{2}{3} = \tikzfig{disconnect}$, while the rest $\matEntry{i}{j}$'s are all $\tikzfig{id-morphism}$.

Proposition <ref> will allow us to simplify our reasoning in the proof of completeness. In light of this result, we will assume  – wherever it is convenient – that we can always rewrite any diagram formed of $\copyy, \discard, \unit, \conjj$ to its equivalent matrix canonical form. This often means that we can be as lax as necessary when identifying diagrams modulo the (co)associativity of $\copyy$ or $\conjj$ and the (co)unitality of $(\copyy, \discard)$ and $(\conjj, \unit)$.

The equational theory of Fig. <ref> contains three commutative and idempotent bimonoids: $(\copyy, \discard, \unit, \conjj)$ as we have already explained, but also $(\copyy, \discard, \codiscard, \cocopy)$ and $(\coconj, \counit, \codiscard, \cocopy)$. Indeed, one can check that the relevant axioms also hold for them: they are easy consequences of (A1)-(A13), (C1)-(C6), and (D1)-(D12). We use the encoding of Boolean matrices using $(\coconj, \counit, \codiscard, \cocopy)$ once in Section <ref>, when translating SAT instances to a diagrams.

Moreover, the canonical form of matrix diagrams provides a simple and formal definition of the intuitive notion of connected wires.

Let $d$ be a canonical matrix diagram as in Definition <ref>.

The $i$-th input wire and the $k$-th output wire are connected if $\matEntry{i}{k} = \tikzfig{id-morphism}$.

The $i$-th and the $j$-th input wires are connected if there exists $k \in \{ 0, \dots, n-1 \}$ such that $\matEntry{i}{k} = \matEntry{j}{k} =  \tikzfig{id-morphism}$.

Intuitively, two wires are connected if there is a path between these two wires.

The notion of two wires being connected is important because when certain wires are not connected, a matrix diagram can be decomposed into smaller matrix diagrams.

Let $d \colon m +2 \to n$ be a matrix diagram. If two input wires are not connected, say input wire $0$ and $1$, then $d$ can be decomposed as follows:

\begin{equation}
\label{eq:mat-decompose}
\tikzfig{mat-diag-fact-4}
\end{equation}

In this proof we will use $\{$ and natural numbers $k$ to indicate that certain pattern appears $k$ many times.

Without lose of generality we assume that $d$ is a canonical matrix diagram.

While one can prove directly on $d$ for arbitrary $m, n$, for clearance we prove by induction on $n$.

If $n = 0$, then (<ref>) is trivial.

Suppose (<ref>) works for arbitrary matrix diagram of type $m+2 \to n$, we show that it also holds for canonical matrix diagram $d \colon m+2 \to n+1$. Since input wires $0$ and $1$ are not connected, wlog we assume that $\matEntry{0}{n} = \tikzfig{disconnect}$ and $\matEntry{0}{n} = \tikzfig{id-morphism}$ (the case where both are $\tikzfig{disconnect}$ is simpler). Then $d$ can be decomposed as follows, where the three green highlighted (matrix) diagrams work respectively as $d_0, d_1, d_2$ in (<ref>):

\begin{equation*}
\tikzfig{mat-diag-fact-5}
\end{equation*}

This finishes the induction step.

§.§ Pre-normal form

In order to rewrite diagrams $m\to 0$ into pre-normal form, we introduce first the notion of traced canonical form for arbitrary diagrams $m\to n$.

Every $\catSyn$-morphism $d \colon m \to n$ has the following traced canonical form:

\begin{equation}
\label{eq:traced-CF}
\tikzfig{traced-CF}
\end{equation}

By bending the right wires of a diagram in traced canonical form to the left, with the mapping $\catSyn[m, n] \to \catSyn[0, n+m]$ provided by Lemma <ref>, we can rewrite any diagram $n\to 0$ into a form that we call existential canonical form.

Proof of Lemma <ref>.
We prove that every $\catSyn$-morphisms is equivalent to one in traced canonical form by induction on the structure of $d$. All the base cases (for generators) are obvious because every generator appears in (<ref>). For the induction step we need to show that if $c$ and $d$ are two morphisms in traced canonical form, then their parallel and sequential compositions are also of traced-canonical form. For parallel composition it is also obvious. As for sequential composition, suppose the types $c \colon k_0 \to k_1$ and $d \colon k_1 \to k_2$, then $c \then d$ is of the following form:

\begin{equation}
\tikzfig{pre-nf-seq-1}
\end{equation}

thus again of traced canonical form.

Next, when we restrict ourselves to diagrams with codomain $0$, we have the following existential canonical form, which are essentially traced canonical normal form diagrams with bended inputs.

Every diagram of type $m \to 0$ is equal to one in the following existential canonical form:

\begin{equation}
\label{eq:pre-NF}
\tikzfig{pre-normal-form-1}
\end{equation}

Notice that existential canonical form diagrams are close to being in pre-normal form: they are pre-normal form diagrams possibly pre-composed with multiple $\cupWhite$. Thus, to prove that every diagram is equal to one in pre-normal form, it suffices to show how to eliminate these $\cupWhite$ from existential canonical form diagrams, while keeping the pre-normal form structure unchanged.

The name existential canonical form comes from a resemblance between this form and quantified boolean formulas in prenex form, with the $\cupWhite$ likened to quantifiers in this analogy. The next proof, which shows how to remove the $\cupWhite$, can be thought of as the diagrammatic counterpart of a quantifier elimination procedure.

Proof of Proposition <ref>.
We pick arbitrary natural numbers $m, n$ satisfying $k = m + n$. Given arbitrary morphism $d \colon k \to 0$, we apply function $q \colon \catSyn[m + n, 0] \to \catSyn[m, n]$ from Lemma <ref>, and get $q(d) \colon m \to n$. By Lemma <ref>, $q(d)$ is of traced canonical form, say (<ref>). Here each $e_i$ is freely generated by the generators in the $i$-th blue box in (<ref>). In this proof we also use the intuitive notation $\tikzfig{oriented-box}$ to specify the orientation of a box, which is important to keep track of when `sliding' along the traces (see <cit.>).

\begin{equation}
\label{eq:canonical-proof-1}
\tikzfig{cor-pre-NF-3}
\end{equation}

Then $d = p(q(d))$ is equivalent to

\begin{equation*}
\tikzfig{cor-pre-NF-2}
\end{equation*}

and the last diagram is of pre-normal form (<ref>).

Proof of Lemma <ref>.
So far we have shown that every diagram $d \colon m \to 0$ is equivalent to some existential canonical form diagram $d'$, and such $d'$ differs from pre-normal form only in that it may possibly be pre-composed with multiple cups (namely $\cupWhite$). So in order to show that every morphism of type $m \to 0$ is equivalent to some pre-normal form diagram, it suffices to prove that all existential canonical form diagrams are equivalent to pre-normal form diagrams by showing that one can eliminate those pre-composed $\cupWhite$ one by one.

Formally, we prove by induction on the number of $\cupWhite$ in existential canonical form diagrams.

We denote the number of $\cupWhite$ in diagram $d$ by $\numCupWhite{d}$.

Let $d \colon m \to 0$ be for existential canonical form.

For the base case, if $\numCupWhite{d} = 0$, then $d$ is already of pre-normal form.

For the induction step, suppose $\numCupWhite{d} = n + 1$, and we have the induction hypothesis (IH): for all existential canonical form morphisms $d'$ with $\numCupWhite{d'} \leq n$, there exists a pre-normal form diagram $d''$ such that $d' = d''$.

Below we eliminate the first $\cupWhite$ from the top. Without loss of generality we suppose $d$ is of the form on the left-hand-side of (<ref>), where $k_1, k_2, k, n$ are natural numbers. In particular, we assume that this presentation `exhausts' all $\copyy$ on the right-hand-side of the top $\cupWhite$: for each wire of the $k_1 + k_2$ wires, there is no $\copyy$ following it. This is always possible because $c$ is a matrix diagram.

Before moving on we solve one simple side case. If one of $k_1$ and $k_2$ is $0$, then the top $\cupWhite$ can be eliminated easily. For example, if $k_2 = 0$, then

\begin{equation*}
\tikzfig{nf-prove-8}
\end{equation*}

So below we assume that $k_1, k_2 \geq 1$.

In this case, we claim that such $d$ is always equivalent to a diagram on the right-hand-side below, where $c'$ is some matrix diagram:

\begin{equation}
\label{eq:nf-prove-7}
\tikzfig{nf-prove-7}
\end{equation}

The key is to study whether those $k_1$ wires and $k_2$ wires are connected with each other.

First, suppose that $k_1, k_2 \geq 1$, and that one of the $k_1$ wires and one of the $k_2$ wires are connected (as inputs to the matrix diagram $c$, see Definition <ref>). Then $d$ is equivalent to

\begin{equation*}
\tikzfig{nf-prove-3}
\end{equation*}

This means that there is a loop in the diagram, which is highlighted yellow as below. As a consequence, we can `delete' these two connected wires without affecting the other $(k_1 - 1) + (k_2 - 1)$ wires, and the resulting diagram is also of pre-normal form.

\begin{equation*}
\tikzfig{nf-prove-4}
\end{equation*}

One can repeat this procedure until there is no two wires from the $k_1$ and $k_2$ wires respectively that are connected. Then by Proposition <ref>, $d$ can be decomposed as

\begin{equation}
\label{eq:nf-prove-10}
\tikzfig{nf-prove-10}
\end{equation}

where $c_1, c_2, c_3$ are all matrix diagrams, and $c_1, c_2$ consist only of $\conjj$ and $\unit$ (namely no $\copyy$ nor $\unit$).

Next, we consider if two of the $k_i$ wires are connected, for $i = 1, 2$. Without loss of generality, suppose two wires among the $k_1$ wires are connected, then indeed these two wires are `redundant' in the sense that the diagram is equivalent to one which has only $k_1 - 1$ copies:

\begin{equation*}
\tikzfig{nf-prove-11}
\end{equation*}

where the second step holds by Proposition <ref>, which proves in particular that (D2) can be strengthened to an equality.
One can repeat this procedure until either $k_i < 2$, or any two wires in the $k_i$ wires are not connected, for $i = 1, 2$. In both cases the $c_1$ and $c_2$ boxes can be `opened':

\begin{equation*}
\tikzfig{nf-prove-9}
\end{equation*}

So far we have proved (<ref>), and we are now ready to eliminate the top $\cupWhite$, using Proposition <ref> and Frobenius equations (B9), (B10):

\begin{equation}
\label{eq:nf-prove-6}
\tikzfig{nf-prove-6}
\end{equation}

Note that the last diagram in (<ref>) is of existential canonical form because the green part is a matrix diagram, whose composition with the matrix diagram $c''$ is again equivalent to a matrix diagram, by matrix completeness (Proposition <ref>). Moreover, it now has only $n$-many $\cupWhite$; thus, by the induction hypothesis it is equivalent to a pre-normal form diagram.

§.§ Downward closed subsets, sets of clauses, pre-normal form

It is helpful to first understand why every diagram with codomain $0$ is equivalent to a pre-normal form diagram, from a semantic perspective.

This amounts to explaining why downward closed subsets of $\Bool^{m}$ are (indeed, precisely) interpretations of pre-normal form diagrams by $\intBProf{\cdot}$.

We first establish the connection between downward closed subsets and

, and then relate the latter with pre-normal form diagrams.

Let $\Var = \{ x_1, x_2, x_3 \}$. The downward closed subset $A_1 = \{ 000, 001, 010 \}$ of $\Bool^{\Var}$ satisfies the  $\{\{x_1\},\{x_2,x_3\}\}$;

the downward closed set $A_2 = \{ 000, 001, 010, 100, 011 \}$
satisfies the  $\{\{x_1, x_2\},\{x_1,x_3\}\}$.

Lemma <ref> together with the discussion below on pre-normal form diagrams and sets of  establish the connection between downward closed subsets and pre-normal form diagrams.

A subset $A \subseteq \Bool^{m}$ is downward closed if and only if there exists some pre-normal form diagram $d \colon m \to 0$ such that $\intBProf{d} = A$.

Proof of Proposition <ref>.
The `if' direction is straightforward. A clause $\{x_{p_1}, \dots, x_{p_{k_i}}\}$ represents the formula $x_{p_1} \land \cdots \land x_{p_{k_i}} = 0$ or, equivalently, $\lnot x_{p_1} \lor \cdots \lor \lnot x_{p_{k_i}} = 1$. It is clear that the set of satisfying assignments of such a clause is downward closed, as we explained in Section <ref>.

For the `only if' direction,

let $S$ be a downward closed subset of $\Bool^{\Var}$.

Let $\Gamma$ be the set of all clauses whose set of satisfying assignments contain $S$ (note that this may be the set containing the empty clause if $S$ is empty). Then clearly, all $\valS\in S$ satisfy $\Gamma$. Suppose that there exists some $\valT\notin S$ which also satisfy $\Gamma$. Then write $\varphi = \{i_1,\dots, i_p\}\subseteq \{1,\dots, m\}$ for the set of components $i_k$ at which there exists $\valS_{k}\in S$ such that $\valS_{k}(i_k)=0 =\lnot \valT(i_k)$ (note that there is at least one such component, otherwise $\valT$ would be in $S$). By construction, elements of $S$ satisfy $\varphi$ while $\valT$ does not. This implies that $\varphi$ must be in $\Gamma$, so $\valT$ should satisfy $\varphi$ too, a contradiction.

Proof of Lemma <ref>.
Note that in the construction of $\diag{\Phi}$, if we have that input wires $i_1, \dots, i_k$ are connected to a $\unit$, then semantically it means that

$\intBProf{\diag{\Phi}} \subseteq \{ \valS \in \Bool^{\Var} \mid  \valS(i_1) \land \cdots \land \valS(i_k) = 1 \}$.

In particular, if $x_i$ does not appear in $\Gamma$, then $\intBProf{\diag{\Phi}}$ contains $\discard$ at the $i$-th input wire, and it implies the trivial condition $\intBProf{\diag{\Phi}} \subseteq \Bool^{\Var}$.

But then $\intBProf{\diag{\Phi}}$ is the intersection of all these sets for each $\gamma \in \Gamma$, which by definition is exactly the

set of satisfying assignments of $\Gamma$.

Consider a

$\Gamma = \big\{\{y^1_1, \dots, y^1_{k_1}\}, \dots,\{y^m_1, \dots, y^m_{k_m}\}\big\}$

a single  $\varphi = \{x_1, \dots, x_n\}$.
If every satisfying assignment of $\Gamma$ also satisfies $\varphi$, then there exists some $i \in \{ 1, \dots, m \}$ such that $\{ y^i_{1}, \dots, y^i_{k_i} \} \subseteq \{ x_1, \dots, x_n \}$.

We prove this by contradiction. Consider a set of clauses
$\Gamma = \big\{\{y^1_1, \dots, y^1_{k_1}\}, \dots,\{y^m_1, \dots, y^m_{k_m}\}\big\}$
and the clause $\varphi = \{x_1, \dots, x_n\}$ such that every satisfying assignment of $\Gamma$ also satisfies $\varphi$. Suppose the lemma does not hold, so that for each $i \in \{1, \dots, m \}$, there exists some $y^{i}_{p_i}$ such that $y^i_{p_i} \not \in \{ x_1, \dots, x_n \}$. Consider the assignment $\valS$ such that $\valS(y^i_{p_i}) = 0$ for all $i \in \{ 1, \dots, m \}$, and $\valS(z) = 1$ for all the other variables. Then it satisfies $\Gamma$: for each $i$, $ \valS(y^i_{1}) \land \cdots \land\valS(y^{i}_{p_i}) \land \cdots \valS(y^{i}_{k_i}) = 0$. However, $\valS$ does not satisfy $\varphi$ because $\valS(x_j) = 1$ for all $j \in \{ 1, \dots, n \}$. This is a contradiction.

Proof of Lemma <ref>.

Since the
satisfying assignments of $\Sigma$ form a subset of those of $\Gamma$,
they are also a subset of the satisfying assignments of every

$\gamma \in \Gamma$.

By Lemma <ref>, for every $\gamma \in \Gamma$ there exists a $\sigma \in \Sigma$ such that $\sigma \subseteq \gamma$.

Using a similar argument, since the satisfying assignments of $\Gamma$ form a subset of those of $\Sigma$, for every $\sigma \in \Sigma$ there exists a $\gamma\in \Gamma$ such that $\gamma \subseteq \sigma$.

Now starting with an arbitrary $\gamma \in \Gamma$, there exists some $\sigma \in \Sigma$ such that $\sigma \subseteq \gamma$, and for this $\gamma$ there again exists some $\sigma' \in \Sigma$ such that $\sigma' \subseteq \gamma$. So $\gamma \subseteq \gamma'$, and for a minimal set of clauses this means $\gamma \subseteq \gamma'$: otherwise we could drop $\gamma'$ and get a smaller set than $\Gamma$ with the same satisfying assignments.

Then $\gamma \subseteq \sigma \subseteq \gamma'$ and $\gamma = \gamma'$ imply $\gamma = \sigma = \gamma'$, which means that $\gamma$ is in $\Sigma$ as well.

Since this holds for arbitrary $\gamma \in \Gamma$, we know that $\Gamma \subseteq \Sigma$.

Applying a similar argument for $\Sigma$, we know that $\Sigma \subseteq \Gamma$.

Therefore we can conclude that $\Sigma = \Gamma$.

Proof of Proposition <ref>
(i) $\iso$ (ii):

It suffices to define two functions between (i) and (ii) which are injective and inverses to each other.

We already know that a subset of $\Bool^m$ is downward closed if and only if it is the set of satisfying assignments to some set of  (Lemma <ref>).

Starting from a downward closed subset $A \subseteq \Bool^m$, one have a least set of  whose set of satisfying assignments is $A$ (Lemma <ref>). Inversely, every set of  uniquely determines a downward closed subset of $\Bool^m$, namely the set of its satisfying assignments.

It follows immediately that these two functions are inverses to each other.

(ii) $\iso$ (iii):

We notice that when restricted to minimal sets of  (resp. normal form diagrams), the images of $\diag{\cdot}$ (resp. $\sysIneq{}{\cdot}$) are normal form diagrams (resp. minimal sets of ). Moreover, two normal form diagrams have the same $\diag{\cdot}$-image precisely when they are equivalent up to commutativity. Thus $\diag{\cdot}$ and $\sysIneq{}{\cdot}$ witness the isomorphism.

Proof of Lemma <ref>

Here the first step uses Proposition <ref>;

the second and third steps use Proposition <ref>.

Consider the pre-normal form diagram $c_1$ from Example <ref>, one can apply Lemma <ref> (to the grey block below) and get a normal form diagram:

\[
\tikzfig{eg-eliminate-redun-ineq}
\]

Proof of Lemma <ref>.
Given a pre-normal form diagram $d \colon m \to 0$ which is not in normal form. By Definition <ref>, this means that in the $n \times m$ Boolean matrix $A$ represented by $d$, there exist two rows $i$ and $j$ such that $A_{ik} \leq A_{jk}$ for all $k = 1, \dots, m$.

Diagrammatically, this means that there is the same pattern as on the lhs of Lemma <ref>: there exists some $\unit$ (the $i$-th one) such that all the input wires that are connected with this $\unit$ is also connected with some other $\unit$.

In this case, we apply Lemma <ref> (from left to right) and turn diagram $d$ into a pre-normal form diagram $e$, whose representing matrix $B$ is of type $(n-1) \times m$, and is essentially $A$ but without the $i$-th row.

Since $A$ is finite, such pattern disobeying normal form can only happen finitely many times, each can be solved by the above procedure. The resulting diagram is of normal form and equivalent to the original diagram $d$.

Proof of Lemma <ref>.
As before, given Lemma <ref> it suffices to prove this statement for morphisms with codomains $0$.

Let $c,d \colon m \to 0$ be two diagrams satisfying $\intBProf{c} = \intBProf{d} = A$, for some a downward closed subset $A$ of $\Bool^{\Var}$ where $\Var = \{ x_1, \dots, x_ m\}$.
By Lemma <ref>, $A$ is the set of satisfying assignments of some

minimal set of clauses, say $\Gamma$.

By Lemma <ref>, $c$ and $d$ are equivalent to some normal form diagrams, say $\nf{c}$ and $\nf{d}$, respectively.

Moreover, $\nf{c}$ and $\nf{d}$ verify $\sysIneq{}{\nf{c}} = \sysIneq{}{\nf{d}} = \Gamma$.

Note that every set of clauses corresponds to a diagram in pre-normal form; when

this set of clauses is minimal, the corresponding diagram is in normal form, by Proposition <ref>.

Now $\nf{c}$ and $\nf{d}$ are both normal form diagrams with semantics $A$, so they are both the normal form diagram uniquely determined by $\Gamma$, the

minimal set of clauses with satisfying assignments $A$.

This means that $\nf{c} = \nf{d}$.

§.§ From diagrams to clauses and back

In Subsection <ref> we explored how to derive a unique set of  from a given diagram with the same semantics and vice versa. Both directions relies on matrix completeness (Proposition <ref>).

Here instead we state how $\sysIneq{}{\cdot}$ and $\diag{\cdot}$ work directly, without using matrix diagrams and their representing matrices as an intermediate step.

On one hand, let $\Phi = \{ \varphi_1, \dots, \varphi_n \}$ be a set of  over $\Var = \{ x_1, \dots, x_m \}$, and we define $\diag{\Phi}$ as follows.

For every  $\varphi \in \Phi$ of the form $\varphi = \{x_{i_1}, \dots, x_{i_k}\}$, one creates a copy (via $\copyy$) of each of the input wires corresponding to the variables $x_{i_1}, \dots, x_{i_k}$, and connect them via $\tikzfig{cup-white-k}$.

In particular, if a variable $x_i$ does not appear in $\Phi$, then we make $0$ copy of the $i$-th input wire by post-composing it with $\discard$, effectively discarding it.

On the other hand, let $d \colon m \to 0$ be a pre-normal form. Moreover, we assume that $d$ is decomposed as $d = d_1 \then d_2$, where $d_1 \colon m \to n$ is a matrix diagram, and $d_2 = (\unit)^n$.

Then we define $\sysIneq{}{d}$ as the following set of  consisting of $n$  over $\Var = \{ x_1, \dots, x_m \}$.

Each $\unit$ in $d_2$ (thus in $d$) generates on  $\varphi$: if $i_1, \dots, i_k$ are all the input wires that are connected with this $\unit$, then $\varphi = \{ x_{i_1}, \dots, x_{i_k} \}$. Then $\sysIneq{}{d}$ is defined as the set of all the  generated by $\unit$ in $d$.

In particular, if no input wire is connected with this $\counit$, then it must be of the form $\tikzfig{white-bone}$, which generates the empty clause

(which has an empty set of satisfying assignments).