Re: [isabelle] Proof by analogy and proof stability in Isabelle



On Thu, Apr 29, 2010 at 5:46 AM, steven at obua.de <steven at obua.de> wrote:
>
> b) Develop a versioning system that not only manages source code (like it is
> currently done) but also content (theories, theorems, proofs, and so on). Part
> of this versioning system is also a mechanism on how to transfer content from
> one version to another

"Transferring content" is exactly what an external representation of
proof objects would allow you to do. A format like Joe Hurd's
OpenTheory is designed primarily for transferring theorems between
completely different theorem provers, but the same idea could also be
useful for transferring theorems between different versions of the
*same* theorem prover.

> And yes, this means
> that at least a part of the versioning system becomes part of the trusted kernel
> of the proof assistant.

The great thing about using proof objects is that you don't need to
trust any new code.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.