A central tension in knowledge representation is between expressiveness and efficiency: the more expressive a language is, the more computationally expensive it is to reason about.
Techniques for maintaining efficiency are akin to techniques for maintaining link integrity in hypertext systems: they are useful and necessary on a limited scale, but must be relaxed at the global scale for the sake of AnarchicScalability.
On the SemanticWeb bus, many different engines will produce proofs for different sorts of problems, but no one engine is expected to be complete for the whole set of problems. Parties are expected to be complete in their ability to follow a proof generated by any other party, and judge whether it is valid.
Parties that don't use logic to justify their data can use digital signatures, and LogicalReflection techniques integrate signatures into the proof system so that trust policies can be manipulated in-band with the rest of the data.
For example:
- The way we choose to resolve this issue is by making the security policy completely general -- access to a page can be described by an arbitrary predicate. This predicate is likely to, but need not, be linked to a verication of identity -- it could be that a particular security policy grants access only to people who are able to present the proof of Fermat's last theorem.. -- section 2.1 Interoperability and Expressivity
of A General and Flexible Access-Control System for the Web. Lujo Bauer, Michael A. Schneider, and Edward W. Felten. To appear in Proceedings of the 11th USENIX Security Symposium, August 2002. among the Proof-Carrying Authentication papers
The access control policy example in the swap/cwm/n3 tutorial provides another example.
example number 3 is left to the reader. That makes PPR:ThreeExamples 
ToDo: refactor stuff from ProofChecking. ToDo: integrate diagrams of the semantic web bus. hmm... XML 2000 slide is not the one DanConnolly was thinking of...
ToDo: justify this in terms of AnarchicScalability; cf www-rdf-rules 4Dec.