MM0 does not itself do any normalization of expressions. Instead, it acts as a verification tool for already completed proofs, although it has some facilities for constructing proofs and it is extensible enough to let you add more automation to it, which you could use to automate normalization tasks. But most likely for some really advanced proof work you would want to use a custom front end language or user interface, and MM0 would come out the back as a way to generate portable and cross-checkable proofs. The facilities of MM0 are mostly designed for ensuring that large and complex systems produce trustworthy results, but it is far outshined by other tools when it comes to aspects of human-computer interaction.
As far as your example is concerned, I think that is a reasonable way to pose a "prove or disprove" question to a high automation system or AI, because the only way to construct a proof of isExample is by proving or disproving the claim. On Tue, Nov 28, 2023 at 7:40 PM Olof <olof.da...@gmail.com> wrote: > Hello! if I sound pretentious, it's because I let chat gpt rewrite my > question in better English :). Anyways: > > Hello! I've recently stumbled upon formal mathematics due to its potential > application in interactive education. Despite delving into the source code > of mm0 and scanning through available documentation, I find it challenging > to fully grasp certain concepts. > > I'm curious about how mm0 handles the normalization/canonicalization of > expressions, if it addresses this at all. My interest stems from its > potential use beyond proof generation, particularly in interactive > scenarios where users may answer questions. Instead of requiring users to > generate entire proofs to demonstrate their abilities, the idea is to allow > users to generate expressions appearing in the proof. The backend then > determines whether that is sufficient to conclude that the user has proven > the provable, thereby eliminating the need to learn the advanced syntax of > proof generation software. The concept involves representing questions as > provable theorems within mm0 using eroteric logic. > > For example, a simple "or" question could be answered by "proving" > (providing selected expressions to) a theorem: > -- Or Inquiry > provable sort ef; -- question > term askOr: wff > wff > ef; > axiom inferOrAnswer1 (a b: wff): $ a $ > $ askOr a b $; > axiom inferOrAnswer2 (a b: wff): $ a $ > $ askOr b a $; > theorem isExample (h: $ a -> b -> c $): $ askOr (~((a -> b) -> (a -> c))) > ((a -> b) -> (a -> c)) $ = '(inferOrAnswer2 (a2i h)); > Some questions only require providing an expression to conclude that the > end user has likely proven a provable, such as questions about solutions to > equations. Tackling this is obviously challenging. How would one approach > it, and does mm0/metamath already implement tools that could be useful to > compare input expressions for "semantic equivalence"? > > -- > 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+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/8fdc51fa-a68b-44af-9c6c-6a7aa68cada5n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/8fdc51fa-a68b-44af-9c6c-6a7aa68cada5n%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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsRfv2GZo_rQuruj8kVfW_71D-%3DhbaESEDHO8DvfeDHoA%40mail.gmail.com.
