The implementation in mmj2 is here:
https://github.com/digama0/mmj2/blob/master/src/mmj/lang/ScopeFrame.java#L154-L294
It does not use the same algorithm as mm-web-rs. I don't have any
particular insights regarding the theoretical properties of the mmj2
algorithm.
On Sun, Apr 2, 2023 at 9:59 PM
I recently implemented a variation on this algorithm for mm-web-rs:
https://github.com/digama0/mm-web-rs/blob/master/src/render.rs#L1026-L1077
As the function name suggests, the thing to google is "clique cover". It is
an NP hard problem, but there are some okay approximations.
On Sun, Apr 2,
Did you try searching things like "search complete subgraphs" ?
Benoît
On Sunday, April 2, 2023 at 1:44:45 PM UTC+2 Glauco wrote:
> What's the algorithm used by mmj2 to represent $d pairs as $d sets ?
>
> For instance, for a given theorem, with yamma I'm producing
>
> $d ph x $. $d k x $. $d k
What's the algorithm used by mmj2 to represent $d pairs as $d sets ?
For instance, for a given theorem, with yamma I'm producing
$d ph x $. $d k x $. $d k ph $. $d j x $. $d j k $.
$d F x $. $d F k $. $d A x $. $d A k $. $d A j $.
whereas mmj2 produces
$d A j k x $. $d F k x $. $d k ph x $.