New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support for automatically figuring out substitutions #46

Open

abchugh opened this issue Jul 14, 2020 · 0 comments

abchugh commented Jul 14, 2020

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:

mmj2/src/mmj/pa/ProofUnifier.java

Line 896 in fc5c242

private void attemptProofOfDerivStep() {

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment