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.
