Talk:A Semantic Wiki for Mathematical Knowledge Management
From semanticweb.org
[edit] Critique: OMDoc vs. Semantic MathML
I've taken a look at this paper because I'm really interrested within representing Math for semantic knowledge management and retrival. But I think that OMDoc is a unpretty solution, because it takes MathML and TEΧ Documents and adds some semantic statements and Landba-Representations.
It might be better to throw it away and create a completly new, fully RDF based, Representation for mathematical Formulas whitch also keeps Landba-Definitions, Units, and a simple Represenation in Mind from the beginning. Such a solution might work more like CAML than the current MathML.
The current solution might be good, but it should work for people like Engineers that are trying to do calculations with it as well. It should also be possible to do transformations and solving formula-systems whitch are overdefined (defining variables whitch are not needed to solve the system).
Clearly, I can't speak for all here, but as an Engineer I have to say that OMDoc is much to complicated for me to handle it properly - and most engineers are not that experienced with Semantics than I am.
See also: Objective-CAML (pdf)
-- MovGP0 20:30, 11 May 2006 (CEST)
- Note that OMDoc is neither a semantic replacement for MathML nor a tool for solving mathematical problems. OMDoc can uses Content MathML or OpenMath for mathematical formulae, but it offers additional layers for statements like theorems, proofs, or examples, and for whole mathematical theories and their dependencies. Your proposed Semantic MathML could be integrated into OMDoc as well, taking the place of Content MathML or OpenMath. Second, OMDoc cannot calculate. One objective in its development has, however, been the interchange of mathematical data between different applications like computer algebra systems or web services. --Langec 01:02, 12 May 2006 (CEST)
- Here again I think we run into the dichotomy of deciding on a canonical form for math data entry and discussion, and xml representations for data sharing on the Semantic Web. I really think a syntax as close to actual math as possible would be best. Even though XML is not S-Expressions, the latter are much easier to use for something that is already complex anyway. And can be transformed into XML reasonably straightforwardly by machine. The advantage of OntoWorld over OMDoc to me is that it is up and running, relatively simple to use, so if we can prototype something here, it could be used as a guide for developing best syntax for future mathematical wikis. And RuleML again is something to consider, but even here it is really a xml representation of prolog which was the alternative to lisp/scheme. That has resolution and backtracking built in. We should try see what has already been done with these original AI languages as a guide for future representations so it does not become even more of a tower of Babel.
- I see that S-expressions are less clumsy to write than XML, but I don't agree with your general critique on OMDoc. OMDoc is not just about writing mathematical expressions. These form just one of the three levels of OMDoc. (Watch out for the "object level" in our paper!) OMDoc's preferred language for mathematical expressions is OpenMath, which is quite clumsy to write, but in fact mathematical expressions could be written in any language -- even in Lisp or some other variant of S-expressions. OMDoc is mainly about mathematical statements and theories, and I don't think that there is an alternative syntax for that. The "human" syntax for mathematical statements is "definition, theorem, proof, example", and OMDoc tries its best to represent this syntax adequately. Besides, OMDoc is "up and running", too (see the OMDoc specification, chapter 26), but not yet in a wiki. The latter is being developed by me right now :-) --Langec 16:17, 30 May 2006 (CEST)
- I don't mean to critique OMDoc (even though I am writing on the Critique page - note I did not create it). Obviously depending on purpose various existing markups have to be chosen. But in general, I think in trying to develop a syntax to use here, we should try to be simple, similar to how we can write links here simply even though it gets converted to RDF, we don't have to write the actual verbose markup. Just as how OntoWorld has pages derived from WikiPedia, but gives deeper granularity, I agree that there should be more specialized semantic wikis for areas like math, chemistry, biology etc that will then have even finer grained details. But we can use what is developed here as a reference. When I say it is up and running I mean as a wiki. I realize you must have already done a lot of work on OMDoc and look forward to seeing it as a wiki also. But we should try to be build on the past if we expect other users to build on our work in the future, otherwise we continue to end up with silos, despite all the markups and schemas which should allow smooth sharing of the data. For instance First and Second Order Logic, Sequent Calculus etc *are* a "human" syntax pre-dating computers which provide an existing syntax for definitions, statements, theorems and proofs. And these have already been represented in languages like scheme, ML, prolog. TPTP I mentioned in another page is one example, the statements are essentially in the latter. It would be great if all these initiatives could dovetail with each other. For instance if you could link to TPTP to get some of your axioms and theorems, then you could focus your time and resources on constructing the theory aspect which is not developed there. And maybe vice versa definitions and theorems you already have that are disjoint from theirs, they could import from your wiki whan it is up as a resource. Then we can end up with something more orderly overall, like the Tower of Hanoi ;-)--USoy
- Hi USoy, I know hardly anything about the representation of definitions, proofs, etc. in 1st/2nd order logics and related languages, but I'm not sure whether these representations resemble the human textbook style, as OMDoc does. Unfortunately, I can't tell you why OMDoc has been invented and why its inventor was not satisfied with other representations… –Langec 10:45, 31 May 2006 (CEST)
- I don't think they are mutually exclusive. Looking at the OpenMath documentation they do seem to have an option (and presumably code) to translate to a prefix notation that looks similar to s-expressions, at least a simpler format than raw xml. See theexample if you click the buttons you can see the same definition as xml, prefix and mathml forms. I guess this is what I'm getting at. Whether we are talking about natural language, logic, xml or a list representation, they are all describing the same objects so in defining user interfaces for math software, we should try to make it ergonomic for the user, and let code transform to other formats depending on use. OMDoc has a particular history and I respect that. But I think the discussion here can help in it's evolution and that of future systems. Logic is used to define definitions in human textbooks, the level of formality depends which one's you are talking about. For instance Principia Mathematica. By ergonomics I don't mean a fancy drag-drop gui, can still be simple text based editing. But the choice of representation affects the user. Probably doesn't matter if it's only a few people doing the data entry, but if it is to be many as it would be on a wiki, then we should try to simplify. For example it could be as easy as:
- Hi USoy, I know hardly anything about the representation of definitions, proofs, etc. in 1st/2nd order logics and related languages, but I'm not sure whether these representations resemble the human textbook style, as OMDoc does. Unfortunately, I can't tell you why OMDoc has been invented and why its inventor was not satisfied with other representations… –Langec 10:45, 31 May 2006 (CEST)
- I don't mean to critique OMDoc (even though I am writing on the Critique page - note I did not create it). Obviously depending on purpose various existing markups have to be chosen. But in general, I think in trying to develop a syntax to use here, we should try to be simple, similar to how we can write links here simply even though it gets converted to RDF, we don't have to write the actual verbose markup. Just as how OntoWorld has pages derived from WikiPedia, but gives deeper granularity, I agree that there should be more specialized semantic wikis for areas like math, chemistry, biology etc that will then have even finer grained details. But we can use what is developed here as a reference. When I say it is up and running I mean as a wiki. I realize you must have already done a lot of work on OMDoc and look forward to seeing it as a wiki also. But we should try to be build on the past if we expect other users to build on our work in the future, otherwise we continue to end up with silos, despite all the markups and schemas which should allow smooth sharing of the data. For instance First and Second Order Logic, Sequent Calculus etc *are* a "human" syntax pre-dating computers which provide an existing syntax for definitions, statements, theorems and proofs. And these have already been represented in languages like scheme, ML, prolog. TPTP I mentioned in another page is one example, the statements are essentially in the latter. It would be great if all these initiatives could dovetail with each other. For instance if you could link to TPTP to get some of your axioms and theorems, then you could focus your time and resources on constructing the theory aspect which is not developed there. And maybe vice versa definitions and theorems you already have that are disjoint from theirs, they could import from your wiki whan it is up as a resource. Then we can end up with something more orderly overall, like the Tower of Hanoi ;-)--USoy
- I see that S-expressions are less clumsy to write than XML, but I don't agree with your general critique on OMDoc. OMDoc is not just about writing mathematical expressions. These form just one of the three levels of OMDoc. (Watch out for the "object level" in our paper!) OMDoc's preferred language for mathematical expressions is OpenMath, which is quite clumsy to write, but in fact mathematical expressions could be written in any language -- even in Lisp or some other variant of S-expressions. OMDoc is mainly about mathematical statements and theories, and I don't think that there is an alternative syntax for that. The "human" syntax for mathematical statements is "definition, theorem, proof, example", and OMDoc tries its best to represent this syntax adequately. Besides, OMDoc is "up and running", too (see the OMDoc specification, chapter 26), but not yet in a wiki. The latter is being developed by me right now :-) --Langec 16:17, 30 May 2006 (CEST)
- Here again I think we run into the dichotomy of deciding on a canonical form for math data entry and discussion, and xml representations for data sharing on the Semantic Web. I really think a syntax as close to actual math as possible would be best. Even though XML is not S-Expressions, the latter are much easier to use for something that is already complex anyway. And can be transformed into XML reasonably straightforwardly by machine. The advantage of OntoWorld over OMDoc to me is that it is up and running, relatively simple to use, so if we can prototype something here, it could be used as a guide for developing best syntax for future mathematical wikis. And RuleML again is something to consider, but even here it is really a xml representation of prolog which was the alternative to lisp/scheme. That has resolution and backtracking built in. We should try see what has already been done with these original AI languages as a guide for future representations so it does not become even more of a tower of Babel.
(conjecture (P != NP))
Well the solution isn't easy but I think the representation is ;-) --USoy
