Alright, great. Moving on, would you consider the following general case of posing a question valid, or do you identify any issues with it? It's evident that the respondent needs to be familiar with the axioms and terms, but that holds true for natural language questions as well, I believe. The extra sorts might be unnecessary, but good for clarity. provable sort e; provable sort ef; term validDomainAnswer: wff > e; term askForDomainAnswer: wff > ef; axiom inferDomainAnswer (a b: wff): $ a $ > $ validDomainAnswer b $ > $ askForDomainAnswer a $; -- a question is provable once a valid answer for it is provable, axiom inferExpressionIsDomainAnswer (a b: wff): $ a $ > $ randomExpressionX $ > $ validDomainAnswer b $; -- randomExpressionX probably contains a and b... dunno... theorem askDomainQuestion (h: $ a $): $ askForDomainAnswer a $ = '(inferDomainAnswer (inferExpressionIsDomainAnswer (manipulateToRandomExpressionX a randomHyps) a) a ); Essentially: Given a what is the askForDomainAnswer answer?
Regarding the normalization of expressions, especially mathematical expressions (QExpr) resembling human input, is it reasonable to apply transformation rules based on previously proven theorems? For instance, whenever a term that is proven to be commutative is encountered, it could be transformed into alphabetical order or a similar arrangement based on those proven theorems. In other words a separate language would state the rules of application of different theorems during the normalization process of different term expressions. This would allow the easy definition of semantic equivalence for various use cases and keep the normalization process connected to the formalization itself. I'm new to this so normalization might be more complex than that but anyways. Is this a valid thought? Is it already implemented somewhere? onsdag 29 november 2023 kl. 02:35:39 UTC+1 skrev [email protected]: > 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 <[email protected]> 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 [email protected]. >> 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/67eb32ec-2e12-4489-a124-354678ee2bcdn%40googlegroups.com.
