Re: Puting MathML in XML document

Dear Filip,

I am working in automated reasoning myself and have worked on such 
matters. The first question you want to pose yourself is whether you 
want to generate presentation MathML (this is what can be directly 
displayed in a browser) or content MathML (better, if you want to be 
able to read the back into a machine and communicate it to other 
machines). Of course content MathML can be converted to presentation 
MathML by standard means (style sheets).

That leaves the question about the markup of AR structures as you have 
tried with your tags. There is already the OMDoc format 
[http://www.mathweb.org/omdoc] that does the same thing and may be 
suitable for your task. Using OMDoc may make your system interoperable 
to others that already use the format.

Maybe you can tell us more about your system.

Michael
-------------------------------------------------------------------------
    Prof. Dr. Michael Kohlhase,         Office: Research 1, Room 62
    Professor for Computer Science      Campus Ring 12,
    School of Engineering & Sciences    D-28758 Bremen, Germany
    International University Bremen     tel/fax: +49 421 200 3140/3103
    http://www.cs.cmu.edu/~kohlhase     e-mail: 
<m.kohlhase@iu-bremen.de>
--------------------------------------------------------------------------



Filip Maric wrote:
> Hello,
> I am working on an automated reasoning system and we have decided to 
> generate all output in XML format. We have made a DTD for validation and 
> XSL for display. I have attached a part of an output and simplified xsl 
> file. At the moment, all the mathematics in the output is enclosed in 
> CDATA tags and is in our internal text format. Now we want to convert 
> the formulas to MathML and I need some help. Is it possible, to modify 
> existing XSL so that it can display MathML formulas in our documents, 
> and if it is, what is the best way to do that. I am using IE5.5 with 
> MathType installed, but I will change browser if it is necessary.
>  
> I appreciate your help,
>  
> Filip Maric,
> Automated Reasoning Group,
> Faculty of Mathematics,
> University of Belgrade
> 
> 
> ------------------------------------------------------------------------
> 
> <?xml version="1.0" encoding="windows-1250"?>
> <xsl:stylesheet version='1.0' xmlns:xsl='http://www.w3.org/1999/XSL/Transform'>  
>  
> <xsl:template match="/">
> <html>
> 	<body>      
> 		<xsl:apply-templates select="argo/trace"/>		
>         </body>
> </html>
> </xsl:template>
> 
> <xsl:template match="trace">
> 	<ol>
> 	<xsl:apply-templates/>
> 	</ol>
> </xsl:template>
> 
> <xsl:template match="goal">
> <li>
>   <table cellspacing="1" bgcolor="#000000" width="80%">
>   <tr>
>     <td bgcolor="#F4F5A1">
>        <code><xsl:value-of select="conjecture"/></code>
>     </td>
>   </tr>
>   <tr bgcolor="#A1CDF5">
>   <td>
>     is <xsl:value-of select="type"/> in 
>     ( <i> 
>       <xsl:for-each select="theory">			
>          <xsl:value-of select="."/>
>       </xsl:for-each>
>       </i>
>     )
>   </td>
>   </tr>
>   </table>
> </li>
> <br/>
> </xsl:template>
> 
> <xsl:template match="truegoal">
> <li>
> <table cellspacing="1" bgcolor="#000000" width="80%"><tr><td bgcolor="#9BE7A4" align="right">The goal has been met</td></tr></table>
> </li>
> <br/>
> </xsl:template>
> 
> <xsl:template match="falsegoal">
> <li>
> <table cellspacing="1" bgcolor="#000000" width="80%"><tr><td bgcolor="#FE5039" align="right">The goal has not been met</td></tr></table>
> </li>
> <br/>
> </xsl:template>
> 
> <xsl:template match="transformation">
> <table class="transformation" width="80%">
> <tr>
> <td width="15%"><xsl:value-of select="@status"/></td>
> <td align="right">by the method <i><xsl:value-of select="@name"/></i></td>
> </tr>
> <tr><td colspan="2" align="right"><code><xsl:value-of select="description"/></code></td></tr>
> </table>
> <br/>
> </xsl:template>
> 
> </xsl:stylesheet>
> 
> 
> ------------------------------------------------------------------------
> 
> <?xml version="1.0" encoding="windows-1250"?>
> <?xml-stylesheet href="argo.xsl" type="text/xsl"?>
> 
> <argo>
> <trace>
> <goal>
> 	<conjecture>
> 		<![CDATA[(:forall (?x)(:forall (?y)(:or (<= ?y ?x ) (<= ?x ?y ) )))]]>
> 	</conjecture>
> 
> 	<type>valid </type>
> 	<theory>PRA</theory>
> </goal>
> 
> <transformation name="Prenex" status="if and only if"/>
> 
> <goal>
> 	<conjecture>
> 		<![CDATA[(:forall (?v_1)(:forall (?v_2)(:or (<= v_{2} v_{1} ) (<= v_{1} v_{2} ) )))]]>
> 	</conjecture>
> 
> 	<type>valid </type>
> 	<theory>PRA</theory>
> </goal>
> 
> <transformation name="Convert Inner Quantifier to Existential" status="if and only if"/>
> 
> <goal>
> 	<conjecture>
> 		<![CDATA[(:forall (?v_1)(:not (:exists (?v_2)(:not (:or (<= v_{2} v_{1} ) (<= v_{1} v_{2} ) ) )) ))]]>
> 	</conjecture>
> 
> 	<type>valid </type>
> 	<theory>PRA</theory>
> </goal>
> 
> <transformation name="Trivial" status="if and only if"/>
> 
> <truegoal/>
> </trace>
> </argo
>

Received on Wednesday, 17 March 2004 23:44:58 UTC