A minor recommendation, but perhaps instead of "." and ".*", you could use "?" and "$", which matches the use in the metamath search command? (Technically "?" only matches one character tokens in metamath search but I think your version is more useful.)
Mario On Wed, Jul 8, 2020 at 2:39 PM Auguste Poiroux < [email protected]> wrote: > Hi! > > Along with our proof assistant, we (OpenAI) are happy to share a simple > search tool for set.mm theorems, available without authentication at: > https://mmproofassistant.azurewebsites.net/search > > This tool offers two ways to search for theorems: by label, or by > hypotheses and conclusion. When searching for a theorem by hypotheses or > conclusion, you can use two RegExp-inspired wildcards: > - . : replaces any Metamath constant or variable (ex: Scalar, A, i^i, > ...). > - .* : replaces any sequence of space-separated Metamath variable or > constants. > > A few example searches that you may find useful:(i) "( ( . + . ) - . ) = > ( ( . - . ) + . )" returns addsub, addsubi and addsubd. > (ii) "mod .* = 0 <->" returns: > - mod0: |- ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( A / B ) e. > ZZ ) ) > - negmod0: |- ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( -u A > mod B ) = 0 ) ) > - absmod0: |- ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( ( abs ` > A ) mod B ) = 0 ) ) > (iii) You can search by hypotheses (by adding search strings prefixed by a > yellow turnstile), "( . -> . )" and "." quickly finds ax-mp (despite the > different ordering of hypotheses). > (iv) Searching for syl3anc, "( . /\ . /\ . ) -> ." and "( ph -> . )" as > hypotheses and "( ph -> . )" as conclusion will work. > > We updated our tutorial with a new Section providing more details about > the search toool: > https://cdn.openai.com/openai_proof_assistant_tutorial.pdf > > We have been using this tool internally for a few weeks now and have been > enjoying it and hope it will help you find theorems more easily as well! > > Auguste > > -- > 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 on the web visit > https://groups.google.com/d/msgid/metamath/9410d276-cf80-498d-87bc-e88295a82839n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/9410d276-cf80-498d-87bc-e88295a82839n%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 on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSs2AB0mmvS3aq9r6LiHFvvnNnqo5uA0_s1odgSUwXQhtg%40mail.gmail.com.
