Linear inferences of size 7 - The Proof Theory Blog

In Anupam’s recent post, he introduced the linear inferences switch and medial. By computational search it had been shown that all linear inferences with 6 or fewer variables are derivable from these two inferences. He also gave an 8 variable linear inference which is not derivable from switch and medial and posed the question of whether this was minimal. Here we answer this by showing that this 8 variable inference was minimal.

A linear formula on a set of variables $X$ is a formula constructed from connectives $\land$ and $\lor$ that uses each variable in $X$ exactly once. A linear inference is then a tautology of the form $\phi \to \psi$ where both $\phi$ and $\psi$ are linear formulae on a set of variables $X$ . In this post we assume these formulae do not contain negation. Of particular interest are the following two linear inferences:

Switch: $a \land (b \lor c) \to (a \land b) \lor c$
Medial: $(a \land b) \lor (c \land d) \to (a \lor c) \land (b \lor c)$

We can then compose these inferences by rewriting, and by applying associativity and commutativity rules. More details on this can be found in Anupam’s post or various papers [1] [2] [3].

Using a correspondence between linear formulae and graphs, we were able to write a search algorithm that was able to verify the following theorem:

Theorem 1. All linear inferences with 7 or fewer variables are derivable from switch and medial.

Corollary 2. The minimal switch and medial independent linear inference has 8 variables.

Linear formulae as graphs

The key insight that allowed searching linear inferences with 7 variables (as opposed to the 6 variables that previous work [4] was able to check) was using a link between linear formulae and graphs. This quotients out associativity and commutativity and so greatly reduces the size of the search space.

For any linear formula $\phi$ , we can associate a (non-directed) graph $\mathcal W(\phi)$ to it as follows:

Let the nodes of $\mathcal W(\phi)$ be the variables of $\phi$ .
Let there be a unique edge between (distinct) nodes $a$ and $b$ if the top-level connective of the minimal subformula of $\phi$ containing $a$ and $b$ is $\land$ , and no edge otherwise.

This second point is clearer with an example. Take the linear formula $\phi$ :

$((a \land b) \lor c) \land d$

$\mathcal W(\phi)$ will have 4 nodes. There is an edge between $a$ and $b$ , as the smallest subformula containing $a$ and $b$ is $a \land b$ , and the top-level connective of this is $\land$ . There is no edge between $a$ and $c$ as the smallest subformula containing them is $(a \land b) \lor c$ , and the topmost connective of this is $\lor$ . The smallest subformula containing $a$ and $d$ is the whole formula, and so there is an edge between them.

Continuing for the rest of the edges, we get the following graph:

Rendered by QuickLaTeX.com

The following theorem makes these graphs useful:

Theorem 3. If $\phi$ and $\psi$ are two linear formulae with the same variables, then there is an inference $\phi \to \psi$ if and only if for all maximum cliques $P$ of $\mathcal W(\phi)$ there is a $Q \subseteq P$ such that $Q$ is a maximum clique of $\mathcal W(\psi)$ .
Proposition 4.4/Theorem 4.6 from [1]

P4-free graphs

Since every linear formula has a corresponding graph, the natural question is whether every graph has a corresponding linear formula. The answer to this question is in fact no. The graphs that correspond to linear formulae are called cographs, which are graphs built inductively from single nodes, disjoint unions, and the dual of disjoint union (taking the union of two graphs and inserting every possible edge between the two halves). Cographs have the following characterization (Proposition 3.6 from [1]).

Definition 4. A graph is P4-free if none of it’s induced subgraphs are isomorphic to

Proposition 5. A graph is P4-free if and only if it is a cograph and hence the graphs that correspond to linear formulae are exactly the P4-free graphs.

This means that we are able to reason about all linear formulae without ever working with any of these formulae, and instead just working with P4-free graphs.

The algorithm

The algorithm is explained in this section by going through step by step. The code is written in haskell and should be semi-readable even without any coding knowledge. The full (commented) code can be found here.

Representing graphs

We represent nodes as integers and then represent a linear graph as function from two nodes (integers) to a boolean which tells us whether there is an edge between the two nodes.

type Node = Int
type LinGraph = Node -> Node -> Bool

Show code

Show less

We also define a second version where the data of a linear graph is packed into a single integer. This is defined as LinGraphC in the code.

Collecting all P4-free graphs

The first step is to collect a list of all P4-free graphs. Since there are 7 choose 2 (= 21) pairs of nodes, there are $2^{21}$ total graphs with 7 nodes. This is too many to run through all the graphs and checking in turn whether each one is P4-free. Therefore we use the following result.

Remark 6. Any induced subgraph of a P4-free graph is P4-free.

Now to generate all P4-free graphs of size $n$ , we can first recursively generate a list of all size $n-1$ P4-free graphs, and then for each of these size $n-1$ graphs, check whether each extension to $n$ variables is a P4-free graph. The base case is then that there is precisely one P4-free graph with no nodes.

This means that large numbers of non P4-free graphs can be discarded at once by noticing that they share a non P4-free induced subgraph.

p4Free :: NoVars -> LinGraph -> Bool
p4Free n lg = all 
             (\ (a,b,c,d) -> not (lg a b && not (lg a c) && not (lg a d) && lg b c && not (lg b d) && lg c d))
             [(a, b, c, d) | a <- [0..(n-1)], b <- [0..(n-1)], c <- [0..(n-1)], d <- [0..(n-1)]]

allP4FreeGraphs :: NoVars -> [ LinGraphC ]
allP4FreeGraphs n
  | n == 0 = [ 0 ] -- There is precisely one empty graph
  | otherwise = do -- Introduces monadic notation, see comments below for the jist of what is happening
      x <- allP4FreeGraphs (n - 1) -- For each graph with 'n-1' variables
      y <- [0 .. (2 ^ (n - 1) - 1)] -- And each combination of 'n-1' bits
      let z = y + (shiftL x (n - 1)) -- Shift the bits for the old variables and add the new ones via addition
      guard ((p4Free n . fromCompressed n) z) -- Check if the generated graph is valid
      return z

Show code

Show less

There are 78416 P4-free graphs with 7 variables.

Finding all linear inferences

The next step is determining for which pairs of graphs $G,H$ , there is a linear inference $G \to H$ . Theorem 3 is used to determine this.

To get all the max cliques of a graph, the Bron-Kerbosch algorithm is used. To avoid having to regenerate the max cliques of each graph, we first run through the entire list of P4-free graphs and store the max cliques for each of these in the following data structure:

type MCliques = [ Set Node ]

Show code

Show less

Then given two graphs along with their sets of max cliques, it is simple to test if there is a linear implication:

linearImplication :: MCliques -> MCliques -> Bool
linearImplication mc1 mc2 = all (\p -> any (`S.isSubsetOf` p) mc2) mc1

Show code

Show less

There are 525109922 total linear inferences between graphs with 7 variables.

Trivial inferences

The next step in the algorithm is to filter out trivial implications.

Definition 7. A linear implication $\phi \to \psi$ is trivial at variable $x$ if $\phi[\bot/x] \to \psi[\top/x]$ is a linear implication.
A linear implication is trivial if it is trivial at any of its variables.

It is not necessary to check trivial inferences because of the following theorem.

Theorem 8. If a linear inference $\rho$ is trivial somewhere then there is a linear inference $\rho^\prime$ on fewer variables that is not trivial anywhere and from which $\rho$ is derivable from switch, medial and units.
Theorem 34 in [2]

As any 6 variable or fewer linear inference is derivable using medial and switch [4], it is immediate from the above theorem that any trivial linear inference with 7 variables is derivable from medial, switch and units.

Further, we have the following lemma:

Lemma 9. If a linear implication $\phi \to \psi$ is not trivial and can be derived from switch and medial, then it can be derived from switch and medial without introducing units.
Lemma 28 from [2]

This will prove helpful when checking whether a given inference is a single switch or medial.

Lastly, we need a way to determine if an inference is trivial using only the graphs. Luckily this is easy given that we already have all the maximum cliques.

Lemma 10. A linear implication $\phi \to \psi$ of graphs is trivial at node $x$ if for all maximum cliques $P$ of $\mathcal W(\phi)$ , there is a set $Q \subseteq P \setminus \{x\}$ such that $Q$ is a maximum clique of $\mathcal W(\psi)$ .
Proposition 5.7 in [1]

and so we can easily check if an inference is trivial with the following code (note that unlike the code for checking an inference, checking triviality crucially depends on the number of variables):

isTrivialAt :: MCliques -> MCliques -> Node -> Bool
isTrivialAt mc1 mc2 x = all (\ p -> any (`S.isSubsetOf` (S.delete <!-- /wp:code -->x p)) mc2) mc1

isTrivial :: NoVars -> MCliques -> MCliques -> Bool
isTrivial noVars mc1 mc2 = any (isTrivialAt mc1 mc2) [0..(noVars-1)]

Show code

Show less

There are 12339852 non-trivial linear inferences between graphs with 7 variables.

Minimal inferences

The next stage of the algorithm is to remove any transitive inferences.

Definition 11. Given graphs $G$ and $H$ , an inference $G \to H$ is minimal if for all graphs $J$ with $G \to J$ and $J \to H$ being inferences, we have that $J = G$ or $J = H$ .

There are three reasons for excluding any transitive inferences:

If there exists an inference which does not derive from switch and medial, then there exists a minimal inference which does not derive from switch and medial. This is because if we have $G \to J \to H$ and $G \to J$ and $J \to H$ both derive from switch and medial, then $G \to H$ also does.
This reduces the number of inferences we have left to check.
A minimal inference must either be a single application of switch or medial, or not be derivable from switch or medial, which is easier to check than checking if an arbitrary inference derives from switch and medial.

The minimal inferences can be found by first collecting all (non-trivial) inferences by their premise. Then for each graph $G$ , the minimal inferences with domain $G$ can be found by taking all graphs $H$ inferred by $G$ and taking away any graphs $J$ such that there is graph $I$ with $G \to I \to J$ being a valid chain of inferences.

getMinimal :: InfGraph -> LinGraphC -> Set LinGraphC
getMinimal ig x =
  let keys = (ig M.! x) -- All the things implied by 'x'
      transitiveImplied = S.unions ((ig M.!) <gt; S.toList keys) -- All the things implied by the things implied by 'x'
  in keys S.\\ transitiveImplied -- 'y's implied by 'x' which are not implied by some 'z' with 'x -> z -> y'

Show code

Show less

There are 524188 (non-trivial) minimal inferences between graphs with 7 variables.

Checking remaining inferences

All that remains is to check the remaining inferences. Because all of these inferences are minimal, it suffices to check whether each one is either a medial or a switch, and because they are non trivial, we do not need to worry about units.

To check if an inferences is an instance of medial we use the following criterion from [5]

Proposition 12. A linear inference $\phi \to \psi$ is derivable from medial iff
Whenever there is an edge between $x$ and $y$ in $\mathcal W(\phi)$ then there is also an edge between $x$ and $y$ in $\mathcal W(\psi)$ ;
Whenever there isn’t an edge between $x$ and $y$ in $\mathcal W(\phi)$ and is one in $\mathcal W(\psi)$ then there are $w,z$ such that we have:
Theorem 5.1 in [5]

Although this criterion checks if an inference is derivable from arbitrarily many medial rewrites, it is sufficient as if a minimal inference is not derivable from medial, then it is either derivable by a single switch or is not derivable from switch and medial.

isMedialStar :: NoVars -> LinGraph -> LinGraph -> Bool
isMedialStar noVars p q = cond1 && cond2
  where
    pairs = [(a,b) | a <- [0 .. (noVars - 1)], b <- [0 .. (noVars - 1)]]
    -- ^ all pairs of nodes
    cond1 = all (\ (a,b) -> if p a b then q a b else True) pairs
    psquare a b c d = p a b && p c d && not (p a c) && not (p a d) && not (p b c) && not (p b d)
    qsquare a b c d = q a b && q c d && not (q a c) && q a d && q b c && not (q b d)
    cond2 = all (\ (a,d) -> a == d || p a d || not (q a d) || any (\ (b,c) -> psquare a b c d && qsquare a b c d) pairs) pairs

Show code

Show less

Therefore all that remains is to check any remaining inferences are a single instance of switch. This is done by iterating through all possible cograph decompositions of the premise and conclusion of the inference and checking if any of them have the right form for a single switch rewrite.

partitions :: [a] -> [([a], [a])]
partitions [] = [([],[])]
partitions (x:xs) = do
  (a,b) <- partitions xs
  [(x:a,b), (a,x:b)]

isAndPartition :: LinGraph -> [Node] -> [Node] -> Bool
isAndPartition lg a b = and [ lg x y | x <- a, y <- b ]

isOrPartition :: LinGraph -> [Node] -> [Node] -> Bool
isOrPartition lg a b = and [ not (lg x y) | x <- a, y <- b ]

isInternallyUnchanged :: LinGraph -> LinGraph -> [Node] -> Bool
isInternallyUnchanged lg1 lg2 xs = and [ lg1 x y == lg2 x y | x <- xs, y <- xs ]

isSwitch :: NoVars -> LinGraph -> LinGraph -> Bool
isSwitch noVars lg1 lg2 = isSwitch' [0 .. (noVars-1)]
  where
    isSwitch' :: [Node] -> Bool
    -- ^ Checks if the inference is given by a switch involving the
    -- nodes in the given set
    isSwitch' xs = flip any (partitions xs) $ \ (a,b) -> -- Search for a partition that satisfies:
      all (not . null) [a,b] -- Check the partition is not trivial
      && conditions a b -- Check further conditions
    conditions a b = cond1 a b || cond2 a b || cond3 a b
    -- ^ must satisfy one of the following three conditions:
    -- Condition one says that the inference is of the form A ∧ B -> A ∧ C where B -> C is a switch
    -- Condition two says that the inference is of the form A ∨ B -> A ∨ C where B -> C is a switch
    -- Condition three says there is a switch involving all the variables
    cond1 a b = isAndPartition lg1 a b -- Formula 1 can be represented 'A ∧ B'
      && isAndPartition lg2 a b -- Formula 2 can be represented 'A′ ∧ B′'
      && isInternallyUnchanged lg1 lg2 a -- 'A = A′'
      && isSwitch' b -- 'B -> B′' occurs as a single switch
    cond2 a b = isOrPartition lg1 a b && isOrPartition lg2 a b && isInternallyUnchanged lg1 lg2 a && isSwitch' b
    -- ^ Same as above but with an or at the top level
    cond3 a b = flip any (partitions b) $ \(c,d) -> -- Further split 'b' into 'c' 'd'
      all (not . null) [c, d] -- This partition was not trivial
      && all (isInternallyUnchanged lg1 lg2) [a, c, d] -- 'a,c,d' are not changed between the formulae
      && isAndPartition lg1 a b
      && isOrPartition lg1 c d -- Formula one has the form 'a ∧ (c ∨ d)'
      && isOrPartition lg2 (a ++ c) d
      && isAndPartition lg2 a c -- Formula two has the form '(a ∧ c) ∨ d'

Show code

Show less

After doing this, it turned out that 428428 of the inferences were switches and 95760 were medials with no other inferences, which completes the proof of Theorem 1.

Checking 8 variables

It would be nice if we were able to take this code and apply it to 8 variables to check that it finds a minimal inference that is not a switch or medial. This would provide some evidence that the code is correct as well as possibly finding more inferences that are not derivable.

However the computational power to check 8 variables is vastly greater than that which was needed to check 7 variables. As written above there are 78416 P4-free graphs with 7 nodes but we were able to calculate that there are 1320064 P4-free graphs with 8 nodes. Assuming we could calculate all the max cliques for all the graphs and store them, we would still run into trouble with the second step of the algorithm which involves checking every pair of graphs for an inference. Even assuming that we can check for an inference between two 8-node graphs in the same amount of time as two 7-node graphs (which is not true as 8-node graphs will in general have more max cliques) then this step will take at least 250 times as long. There are also a lot more stages of the algorithm after this.

The current algorithm takes around 10 minutes to run on a relatively powerful desktop, and so 8 variables was out of our reach though it is possible someone with a more powerful computer or more time could attempt to run the code. It is also possible that there are some easy time savings, for instance quotienting out by graph isomorphism in the premise of each inference, though we could not work out how to implement this nicely.

References

[1]

A. Das and L. Strassburger, “On linear rewriting systems for Boolean logic and some applications to proof theory,” Logical Methods in Computer Science, vol. 12, iss. 4, 2017.
[Bibtex]

@article{Das_2017,
title={On linear rewriting systems for Boolean logic and some applications to proof theory},
volume={12},
ISSN={1860-5974},
url={http://dx.doi.org/10.2168/LMCS-12(4:9)2016},
DOI={10.2168/lmcs-12(4:9)2016},
number={4},
journal={Logical Methods in Computer Science},
publisher={Logical Methods in Computer Science e.V.},
author={Das, Anupam and Strassburger, Lutz},
editor={Fernandez, MaribelEditor},
year={2017},
month={Apr}
}

[2]

A. Das, “Rewriting with Linear Inferences in Propositional Logic,” in 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Dagstuhl, Germany, 2013, p. 158–173.
[Bibtex]

@InProceedings{das:LIPIcs:2013:4060,
author =  {Anupam Das},
title =  {{Rewriting with Linear Inferences in Propositional Logic}},
booktitle =  {24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
pages =  {158--173},
series =  {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN =  {978-3-939897-53-8},
ISSN =  {1868-8969},
year =  {2013},
volume =  {21},
editor =  {Femke van Raamsdonk},
publisher =  {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address =  {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/4060},
URN = {urn:nbn:de:0030-drops-40609},
doi = {10.4230/LIPIcs.RTA.2013.158},
annote =  {Keywords: proof theory, propositional logic, complexity of proofs, deep inference}
}

[3] C. Calk, A. Das, and T. Waring, Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs, 2020.
[Bibtex]

@misc{calk2020formulasascographs,
title={Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs},
author={Cameron Calk and Anupam Das and Tim Waring},
year={2020},
eprint={2004.12941},
archivePrefix={arXiv},
primaryClass={cs.LO}
}

[4] A. Šipraga, “An automated search of linear inference rules,” Research project. Supervised by Alessio Guglielmi and Anupam Das, 2012.
[Bibtex]

@article{Sip12:automated-search,
title={An automated search of linear inference rules},
author={Alvin \v{S}ipraga},
year={2012},
journal={Research project. {S}upervised by {A}lessio {G}uglielmi and {A}nupam {D}as},
url={http://arcturus.su/mimir/autolininf.pdf}
}

[5] L. Straßburger, “A Characterization of Medial as Rewriting Rule,” in Term Rewriting and Applications, Berlin, Heidelberg, 2007, p. 344–358.
[Bibtex]

@InProceedings{10.1007/978-3-540-73449-9_26,
author="Stra{\ss}burger, Lutz",
editor="Baader, Franz",
title="A Characterization of Medial as Rewriting Rule",
booktitle="Term Rewriting and Applications",
year="2007",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="344--358",
abstract="Medial is an inference rule scheme that appears in various deductive systems based on deep inference. In this paper we investigate the properties of medial as rewriting rule independently from logic. We present a graph theoretical criterion for checking whether there exists a medial rewriting path between two formulas. Finally, we return to logic and apply our criterion for giving a combinatorial proof for a decomposition theorem, i.e., proof theoretical statement about syntax.",
isbn="978-3-540-73449-9"
}

3 thoughts on “Linear inferences of size 7”

Anupam Das says:

October 8, 2020 at 9:20 pm

Even though we discussed this before, I feel compelled to comment… Well done Alex! This question has been bugging me for years so, along with my previous post, it is nice to finally have resolution :).

As you point out, a previous attempt [4] hit computational barriers at 6 variables. It is nice to see that some of the graph theoretic work done in the intermediate years was useful for this algorithm to become feasible at 7 variables.

Alessio Guglielmi says:

November 28, 2020 at 7:30 pm

Nice job, Alex.

Do you think that it would be possible to use your technique to help to design a proof system directly on relation webs and disregarding N-freeness? That proof system would have switch and medial but it wouldn’t be restricted to formulae, and therefore would not suffer, in principle, from the limitations discovered in [1].

The other requirement of the system would be, of course, that it only produces sound inferences between formulae. What exactly is a switch and a medial would be open to design choices, but again, they should behave as switch and medial on formulae.

In other words: would enriching the language solve the problem of poor expressivity that we observe over formulae?

1. Anupam Das says:
  
  November 30, 2020 at 3:52 pm
  
  As one answer to your question Alessio, you may be aware of work I did with some students, Cameron Calk and Tim Waring: https://arxiv.org/abs/2004.12941 . I did not yet get around to producing a proof theory for the logic, but it is indeed conservative over Boolean logic, and there are reasonable generalisations of switch and medial.
  
  The hope is, indeed, to escape the limitations from [1]. That result does not apply to the arbitrary graph-theoretic setting, but I do not know if there is a complete ‘linear’ system.
  
  Also notable is the work of Matteo Acclavio, Ross Horne and Lutz Strassburger, who embark on a similar investigation for the case of MLL: https://hal.inria.fr/hal-02560105 . They focus on a proof theoretic approach, giving a cut-elimination result using a graph-theoretic version of splitting. Interestingly, their logic is incomparable with the one from my paper, and we do not really understand why.

Linear formulae as graphs

P4-free graphs

The algorithm

Representing graphs

Collecting all P4-free graphs

Finding all linear inferences

Trivial inferences

Minimal inferences

Checking remaining inferences

Checking 8 variables

References

3 thoughts on “Linear inferences of size 7”

Leave a Reply Cancel reply