Sent from Mail<https://go.microsoft.com/fwlink/?LinkId=550986> for Windows

From: Glauco<mailto:[email protected]>
Sent: 22 August 2022 19:36
To: Metamath<mailto:[email protected]>
Subject: [Metamath] Re: MMJ question


  *   some code is spent on computing max array size.


  *   it may be Java back then didn't have the variable length ADTs


  *   Robinson's mgu finder.
  *

If U is the most general 
unifier<https://encyclopedia2.thefreedictionary.com/unifier> of a set of 
expressions
then any other unifier, V,
can be expressed as V = UW,
where W is another substitution.

What’s the best thing to read to grok this algorithm?
MMJ? But I don’t know Java, so is there an algorithm in English?

thx

-- 
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, send an email 
to [email protected].
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/CO3PR18MB49608C696D935ACE3E8DBE59A4719%40CO3PR18MB4960.namprd18.prod.outlook.com.

Reply via email to