I would like to use the Thot library for building a front end to our interactive
theorem prover system ILF (http://www-irm.mathematik.hu-berlin.de/~ilf).
The aim would be to create an editor for restructuring proof presentations. The
proofs have a rather simple tree-with-links like structure.
The main problem I face is to write something similar to the html2thot converter
used in amaya to import the internal proof presentation used by our system
(prolog based) and to convert it to the PIV format. Unfortunately there does not
seem to exists a high level interface similar to a transformation schema.
Here are my questions:
Is there any chance that such an interface is developed in the near future?
If not, is it possible for an 'outsider' to write a low level converter in an
acceptable amount of time?
If so, where can I get information about the internal format used by Thot?
Thank you for any replies,
Thomas