[SCL] What we need to do NOW.

[geoff at cs.miami.edu]

Hi,

> 3. We need a concrete XML syntax (as vanilla as possible). This may 
> be straightforward, but if anyone has any strong feelings about 
> appropriate XML 'style' then please express them, or preferably 
> design an XML syntax according to your preferred style.

You may like to look at the XML of Petr Pudlak, who has a tool to translate
my TPTP and TSTP syntaxes to XML. He says ...

> I've had some time to work on my TSTP parser recently, so here is what
> I've done so far. I created TSTP representation in XML, with document
> structure much the same as the TSTP. I didn't finish DTD file for it,
> but I've already parsed almost all of the TPTP library, so it is
> possible to view the results. The converted TPTP library can be found at
> 
>   http://lipa.ms.mff.cuni.cz/~pudlak/tstp2xml/
> 
> I've also prepared some demo java application that converts TSTP to XML.
> It can be run using Java WebStart (supplied with JRE1.4), just put
> 
>   http://ktilinux.ms.mff.cuni.cz/~pudlak/tstp2xml/tstp2xml.jnlp
> 
> into the location field in the WebStart manager (the web server is not
> configured properly, so just clicking on the link might not work). The
> application can open/edit TSTP file, then convert it into XML and save
> it.
> 
> What I want to do next is to add parsing headers of the TPTP/TSTP files,
> and then to work on the reverse translation from XML to TSTP. It seems,
> that it is be possible to do it just using XSL stylesheet, so this
> reverse conversion would be completely language idependent.
> 
> I thing this XML format might be useful for other people, so if you know
> anybody interested, please let him know about it.

... and ...

> I you want to try something now, try the GUI demo using webstart, or
> directly download the
> 
>   http://ktilinux.ms.mff.cuni.cz/~pudlak/tstp2xml/tstp2xml.jar
> 
> archive. When executed, it processes every TPTP/TSTP file on the command
> line and converts it to XML. With no arguments, it works as a pipe.

I have CCed this to Petr, and also to Juergen Zimmer who has a strong
interest in this XML-for-ATP issue.

Cheers,

Geoff

Geoff Sutcliffe                           http://www.cs.miami.edu/~geoff
Department of Computer Science            Email : geoff at cs.miami.edu
University of Miami                       Phone : +1 305 2842158/2842268
(Director of Undergraduate Studies)       FAX   : +1 305 2842264