Distributed Tagging and Annotation of Computer-Checked Proofs
Eliot Setzer
Abstract:
Users of theorem proving systems often complain about lemma management
issues within their own proofs and have even more difficulty locating
and reusing appropriate definitions and formalized theorems available
from third parties. Both users’ searches for and understanding
of lemmas can be improved by associating relevant metadata with portions
of formal proofs. This paper describ es an architecture based on web
annotation techniques intended to lower the barriers to
spur-of-the-moment and collaborative creation of metadata for formal
proofs. The architecture allows user annotations and both user-defined
and automatically generated tags to be represented in a unified and
prover-agnostic way.