Greetings, tried to find a definition for proof generation from a list of statements/expressions+justifications+dependencies.
mmj2, metamath.exe, yamma, metamath-lamp, all generate valid proof statements, but could not find a spec on the requirements that they implement. Is a spec available, even if informally? Best regards. -- 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/e3b5b65e-1c4c-4f88-9ae1-a69e74b0ca0cn%40googlegroups.com.
