[opentheory-users] lambda terms vs articles

[Ramana Kumar]

Hi OpenTheory list!

I have a question about the fundamental proof representation format used by
OpenTheory:

Why not lambda terms?

I am inspired by the proof terms available in the Isabelle theorem prover.
If one reads Berghofer and Nipkow's work on proof terms, they recount a
number of reasons to prefer lambda terms to a flat unstructured sequence of
commands for a virtual machine. Mostly these advantages come in the form of
being able to re-use results from areas such as type checking and term
rewriting more easily in the compression of proofs. (Apart from technical
reasons, there are probably also social reasons for making things appealing
to a wide group of smart people.)

Now, it may be that in practice these supposed advantages of proof terms
don't show up. Was the OpenTheory design chosen after a careful comparison,
or was it just a matter of using something familiar and straightforward?

Cheers,
Ramana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150917/c270ccd3/attachment.html>