Stating formalisms in XML adds the interoperability benefit of XML to them. Existing tools for formal methods are based on a particular implementation of the semantics of the computational model in a tool-specific format. This complicates interoperability. Instead we propose to use XML also for representing the semantics and even provide a tool for its execution.

We describe how a formalism can be "XMLized"; and not only expressions in the formalism but also the semantics. The recipe for doing this consists of (1) choosing or defining a suitable XML vocabulary for expressions and (2) defining transformation rules capturing the semantics.

The transformation rules themselves are specified in a mix of XML from the problem domain and the Rule Markup Language (RML) we designed. We introduce the idea of using "Regular XML Expressions" for matching and binding variables in the input of a rule, and to use those variables in the output of a rule. The input and output of a transformation are in pure problem domain XML. With this rulebased approach we can define and perform transformations that are very hard to do with other techniques, for instance XSLT, the W3C Recommendation for XML transformations. A sequence of transformations can be used for simulations and proofs, as demonstrated by an example that shows the derivation of a proof in propositional logic, taking MathML as the problem domain XML. This process is easy to automate and leads to a general purpose theorem prover for XML based formalisms. The RML transformation tool that can reproduce the MathML example in the paper is available from the authors.