Hi, Il 22/06/19 16:21, Jon P ha scritto: > A friend who has some nice programming skills has been working with me > on a search engine for set.mm. We'd really appreciate any feedback if > anyone is willing to check out the first draft which we've done, do you > like it? Is it useful? Can you find theorems you look for? You can click > on your name to see your author page too :)
The idea is undoubtedly wonderful (and demand for Metamath searching tools is definitely less than offer, for the time being), however, like DAW, I also find that results are not what I would expect from the query. Also, a fantastic thing to have would be a matching that know how Metamath work, and for example is able to replace variables, or match subtrees of formulae. Of course that would be much more work than just throw the Metamath database into a stock searching engine. Or maybe not, I have no idea. But please do not interpret my remarks as discouraging: it is very nice to have someone working on this and I am sure that with some work this can become a very valuable tool. Giovanni. -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- 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/b721fb8c-2bc4-785b-6ceb-21a57a7326ed%40gmail.com.
signature.asc
Description: OpenPGP digital signature
