It's really great to see Rumm being used, and so successfully!
In https://github.com/metamath/metamath-knife/issues/87 Mario pushed back on the idea of having metamath-knife supporting Work Variables, I'd need to dig up the proposal made at that time and see what can be done. On 14/01/2025 13:54, Gino Giotto wrote:
I made two Rumm tactics capable of finding proofs in propositional logic. The goal statements can be of any shape you like, but they must be expressed with primitive symbols only (implication and negation). The generated proofs are in the Metamath compressed format. These tactics can find proofs of theorems with no hypotheses or rules of inferences that have at most one hypothesis. Example of a proof found by one of the tactics: mine_ancom $p |- -. ( ( -. ( ph -> -. ps ) -> -. ( ps -> -. ph ) ) -> -. ( -. ( ps -> -. ph ) -> -. ( ph -> -. ps ) ) ) $= ( wn wi idd notnotrddd impneg ax-1 notnotd jcnd expi notnoti split ) ABCZ DCZBACZDCZDQODZCANQABQABQOBPANBABBABEFGOAANAABAABHFGIJKFGRBPOBAOBAOQANBPA BAABAEFGQBBPBBABBAHFGIJKFGLM $. I put the tactics here https://github.com/GinoGiotto/mm-tactics, as well as some auxiliary files. Hopefully it looks clear and intuitive to understand. Rumm is a language created by Thierry Arnoux, aimed at writing tactics to automatically generate Metamath proofs. The specification is available here: https://github.com/tirix/rumm/blob/master/rumm.md. The language is still primitive and some mechanisms are somewhat odd, but I added a few relevant notes in the specification that should help to speed up your learning journey, at least making it faster than mine. Both tactics have been tested against 112 theorems present in set.mm, and both of them successfully found proofs for all combined goals in a few seconds. Moreover, I added 4 long bonus statement as stress testing, and they also worked in a few seconds, so the heuristic looks promising (of course this doesn't rule out the possibility of mistakes). Reading around, it seems that the common approach to tackle this kind of problem is to reduce the statements into conjunctive normal form. I did not do that. Instead, I used an "implicational normal form", which doesn't seem to be very popular given the scaricity of results in my google searches. In the end, I took the basics from this short paper https://www.jstage.jst.go.jp/article/jafpos1956/4/2/4_2_151/_pdf and then I figured out some technical procedures by myself. The generated proofs are, of course, far from optimal, and sometimes quite long. However, one can apply the minimizer afterwards, shortening them significantly. Can these tactics be expanded to support the other propositional symbols as well? In principle yes. However, there is an important issue that is stopping me from going further: Rumm does not support work variables. This is problematic for many different reasons, some of which I explained in more details in this issue: https://github.com/tirix/rumm/issues/12. I tried a few hacks to "simulate" them, but for me it never worked. If someone has ideas I will welcome them with pleasure. Most information I know about work variables comes from here https://github.com/digama0/mmj2/blob/master/doc/WorkVariables.html, with the addition of some conversations with Thierry. Rumm however, uses a strange kind of pseudo work variables system which somewhat works in some situations but not really, and caused in me many headaches. There is currently an open PR to add work variables in metamath-knife, which could be a start https://github.com/metamath/metamath-knife/pull/89. I do believe that supporting work variables would make all the difference, playing a crucial role in Rumm's usability. To create these propositional provers, I circumvented the problem. My tactics use auxiliary theorems that I added with the purpose of avoiding ~ax-mp or ~syl theorems, which would have required work variables. The auxiliary theorems are in the .mm files in the mentioned repository. Using tactics in Metamath has great potential, and I hope that my toy work sparked some curiosity. The long term idea (also said by Thierry) would be to have a tactics file in the set.mm repo with basic CI (like label renaming), and progressively build more complex tactics from simple ones. I'm convinced that tactics would speed up Metamath progress exponentially. -- 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 visit https://groups.google.com/d/msgid/metamath/c2a6948b-fb53-4f13-9ad3-9b8ed9104a8an%40googlegroups.com <https://groups.google.com/d/msgid/metamath/c2a6948b-fb53-4f13-9ad3-9b8ed9104a8an%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- 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 visit https://groups.google.com/d/msgid/metamath/f88d2c9b-45e5-408c-8495-46bbaa5d36ca%40gmx.net.
