Tactics for finding Metamath proofs in propositional logic

[Gino Giotto]

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.

[Thierry Arnoux]

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.

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/c2a6948b-fb53-4f13-9ad3-9b8ed9104a8an%40googlegroups.com.

[Glauco]

Hi Gino,

is there a "formal" definition of tactic?

Could it be represented by an interface to be implemented? An abstract (OOP) class to be extended?

Thanks in advance

Glauco

[Gino Giotto]

> Hi Gino,

> Is there a "formal" definition of tactic?

I'm afraid I can't be of much help here, since I'm just the end user. For a formal definition you're probably better off asking the experts (Thierry, Mario etc.).
In the MM1 description https://github.com/digama0/mm0/blob/master/mm0-hs/mm1.md it's mentioned that its tactics language is close to Scheme (in the Lisp family), so that could be a starting point to find useful sources.

Quote: <<The key new capability of MM1 over MM0 is the inclusion of a Turing-complete programming language over MM0, a lisp dialect similar to Scheme. Proofs of theorems are given as s-expressions, which may be constructed by lisp programs, also known as "tactics" in this context.>>

> 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.

I won't hide that support for work variables would make me very happy, but if it doesn’t pan out, well.. I did my best :)

[Mario Carneiro]

(Note: I have been on holiday since christmas, so sorry for any delayed responses and feel free to re-ask any questions which I missed.)

Just to clarify on the above point: I was not advocating against work variables (metavariables) in metamath-knife, I was advocating against metavariable support in the `Formula` type that mm-knife uses for completed proofs. I think metavariables and other proof assistant features should be supported via another type e.g. `MetaFormula` which is a superset of `Formula`. The data structures you want to use for in-progress proofs are rather different from what you use for completed proofs. But as a result of that, a module for handling MetaFormulas would be essentially a separate thing from the rest of mm-knife, and it's not yet clear whether there are benefits for having it in mm-knife itself, compared to if it was a data type defined by a downstream crate with its own concepts of elaboration and tactic execution (which interact with unification etc and need to use MetaFormulas in a variety of ways).

[Gino Giotto]

A few months ago I opened this Rumm issue. It involves a bug that, if solved, would allow me to get around the lack of work variables. Perhaps that's a simpler solution?

It wouldn't be as good as having work variables, but it would be better than nothing. At least, I would have a hack to finally support the kind of tactics that are currently impossible to implement without them.