Thanks Benoit and Mario,
it looks like we've plenty of algorithms to chose from. I'm going to do
some research and pick one.
Glauco
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it,
Thanks Benoit and Mario,
it looks like we've plenty of algorithms to chose from. I'm going to do
some research and pick one.
Glauco
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it,
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