Here are the QEDEQ syntax descriptions for the prototype which didn't have the full scope of the main project. The prototype has it's own proprietary format.

Module	definition of a QEDEQ module
Formula	definition of a QEDEQ formula
Example 1	QEDEQ module with axioms of propositional calculus, an example for a QEDEQ module
Example 2	QEDEQ module including proofs, another example
Text	definition of a text style QEDEQ module in BNF notation

update 2006-09-13 19:53:34+0200