Open abchugh opened 3 years ago
I am looking for a way to automatically figure out the substitutions required to be able to convert a theorem to a provided statement. This is needed so that we don't need to manually create substitution maps like this for generating automation: https://github.com/Sophize/METAMATH_SERVER/blob/master/src/main/java/org/sophize/metamath/server/machines/NNSumMachine.java#L273
Mario suggested that this is called 'unification' and provided this link: https://github.com/digama0/mmj2/blob/fc5c2427d3d0e0f56c392ae2603ca362dfec3e02/src/mmj/pa/ProofUnifier.java#L896
It would be great if we could get a simple interface that takes a theorem and a statement as input and returns a substitution map.
I am looking for a way to automatically figure out the substitutions required to be able to convert a theorem to a provided statement. This is needed so that we don't need to manually create substitution maps like this for generating automation: https://github.com/Sophize/METAMATH_SERVER/blob/master/src/main/java/org/sophize/metamath/server/machines/NNSumMachine.java#L273
Mario suggested that this is called 'unification' and provided this link: https://github.com/digama0/mmj2/blob/fc5c2427d3d0e0f56c392ae2603ca362dfec3e02/src/mmj/pa/ProofUnifier.java#L896
It would be great if we could get a simple interface that takes a theorem and a statement as input and returns a substitution map.