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 is a formula constructed from connectives
and
that uses each variable in
exactly once. A linear inference is then a tautology of the form
where both
and
are linear formulae on a set of variables
. In this post we assume these formulae do not contain negation. Of particular interest are the following two linear inferences:
- Switch:
- Medial:
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 , we can associate a (non-directed) graph
to it as follows:
- Let the nodes of
be the variables of
.
- Let there be a unique edge between (distinct) nodes
and
if the top-level connective of the minimal subformula of
containing
and
is
, and no edge otherwise.
This second point is clearer with an example. Take the linear formula :
will have 4 nodes. There is an edge between
and
, as the smallest subformula containing
and
is
, and the top-level connective of this is
. There is no edge between
and
as the smallest subformula containing them is
, and the topmost connective of this is
. The smallest subformula containing
and
is the whole formula, and so there is an edge between them.
Continuing for the rest of the edges, we get the following graph:
The following theorem makes these graphs useful:
Theorem 3. If
Proposition 4.4/Theorem 4.6 from [1]and
are two linear formulae with the same variables, then there is an inference
if and only if for all maximum cliques
of
there is a
such that
is a maximum clique of
.
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.
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 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 , we can first recursively generate a list of all size
P4-free graphs, and then for each of these size
graphs, check whether each extension to
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.
There are 78416 P4-free graphs with 7 variables.
Finding all linear inferences
The next step is determining for which pairs of graphs , there is a linear inference
. 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:
Then given two graphs along with their sets of max cliques, it is simple to test if there is a linear implication:
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
is trivial at variable
if
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
Theorem 34 in [2]is trivial somewhere then there is a linear inference
on fewer variables that is not trivial anywhere and from which
is derivable from switch, medial and units.
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
Lemma 28 from [2]is not trivial and can be derived from switch and medial, then it can be derived from switch and medial without introducing units.
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
Proposition 5.7 in [1]of graphs is trivial at node
if for all maximum cliques
of
, there is a set
such that
is a maximum clique of
.
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):
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
and
, an inference
is minimal if for all graphs
with
and
being inferences, we have that
or
.
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
and
and
both derive from switch and medial, then
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 , the minimal inferences with domain
can be found by taking all graphs
inferred by
and taking away any graphs
such that there is graph
with
being a valid chain of inferences.
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
is derivable from medial iff
Theorem 5.1 in [5]
- Whenever there is an edge between
and
in
then there is also an edge between
and
in
;
- Whenever there isn’t an edge between
and
in
and is one in
then there are
such that we have:
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.
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.
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
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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}
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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}
}
[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}
}
[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}
}
[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"
}
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.
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?
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.