All Programs Infer
A key feature of XLogic, which will come out in the earliest formal models, is that all programs do inferences, its not just about that special class of programs which we think of as proof tools.
So XLogic does not major on the implementation of proof tools, or even on the integration of existing proof tools into XLogic (though both of these figure).

XLGlue
Sometimes called XLGlue, sometimes a metainference tool.
The metainference tool is there to sew together arguments from pieces implemented in different languages, and to keep track of the resulting level of confidence (depending on the confidence with which the pieces were demonstrated.
The early stages of metamodelling will provide the basis for a simple metainference tool, which should not be greatly impacted by the later stages.
So a first XLGlue prover should follow on fairly rapidly from the first metamodels.


Proof Tool Integration
Apart from a very simple metainferrer there is no intention to build proof tools under XLogic.
Integration of existing tools into the framework is more likely.
The first one is ProofPower, which is the one best supported (so far as literate scripts are concerned) at present.
What integration involves is not so clear at present.
The first desideratum is that tools should deliver signed claims about the truth of documents in certain languages, but it is probably that this could be realised by another bit of XLGlue providing a wrapper which does packages up and signs the results from a proof tool.
The next stage of integration would involve proof tools accepting and inferring from signed XLogic claims.


