Re: inference rule markup?

Dears, 
	the formalization problem you mention seem to have a 
quite general nature. 
The former MathMl WG is currently formalizing the new charter
proposal. If you have any interesting idea or suggestion to
approach MathML to your activities, I would strongly suggest 
you to contact the main responsibles of MathML. 
(I send a copy in CC to Patrick Ion).

Best wishes.
					-- andrea

On Wed, 14 Feb 2001, Dan Connolly wrote:

> Philip Wadler wrote:
> > 
> > I would be interested in formalizing both MSL and the query algebra.
> > 
> >         MSL:
> >         http://www.cs.bell-labs.com/who/wadler/topics/xml.html#msl
> > 
> >         Query algebra:
> >         http://www.cs.bell-labs.com/who/wadler/topics/xml.html#xalgebra-icdt
> >         http://www.w3.org/TR/query-algebra
> 
> Yes... exactly... me too; I see the latter is available as PDF;
> I'd like to know how you produce it. I suspect you use latex
> and some idioms/macros for grammars and inference rules
> (and a few other notational idioms). If you'll point
> me to some documentation of those tex/latex idioms
> [I've been searching/surfing/googling without much luck]
> and maybe let me look at the tex source of that algebra
> paper, I'll try to design some XHTML/MathML dialect
> that
> 
> 	* can be machine-translated (using XSLT or something)
> 		to larch/coq/boomborg-pc for proof-checking
> 
> 	* can be machine-translated to TeX for all the things
> 		that TeX is good for (printing, submitting to
> 		journals, etc.)
> 
> 	* can be edited in direct-manipulation fashion with Amaya
> 		and/or Andrea's MathML editing tool and/or
> 		other XML editing tools.
> 
> oh... and of course, the semantic-web angle:
> 
> 	* has its terms grounded in URI-space
> 
> -- 
> Dan Connolly, W3C http://www.w3.org/People/Connolly/
> 

Received on Wednesday, 21 March 2001 07:37:18 UTC