On Mon, May 11, 2009 10:22 pm, Lars Hellström wrote: >> The reason I say that is what you have is really a (part of) a proof >> here, >> especially when one looks at the annotations. > > Indeed, or at least the skeleton of (part of) a proof. In my case the > annotations would mainly specify which identity is applied and where > (which is not at all obvious -- especially for derivations that employ > previously derived rules). > >>> * There are several steps in this thing, yet it constitutes >>> a natural unit (in whatever document it is part of). >> Quite. It is a 'proof' and could be a free-standing Lemma. One might not >> wish to do so for expositional reasons, but a proof ought to be capable >> of being a chain of sub-proofs. >>> * Not all steps employ the same relation. >> True, but, and this is the hard part to formalise, they must be >> "logically compatible". > Well, I don't see much point in formalising that; it must in the end be > up to the party who constructs this kind of proof to draw some logical > conclusion from it. Attempts to construct a syntactic description of > the cases where this is possible are likely to be futile. Which is one reason I didn't like the syntactic n-ary relation. But one wishes such a chain to be such that a "sufficiently clever" verifier could verify it, and one probably wants some subset of such prrofs to be verifiable by pretty simple verifiers.
>>> PS: While typing up the example, I noticed that it probably wouldn't be >>> correct since limit1#tendsto (MathML3-ish?) is defined to be ternary, >>> requesting a type-of-limit as first argument. While I suppose one could >>> use a lambda to work around that, I can't help wondering why the limit >>> type is an argument in the first place; wouldn't an attribution be more >>> appropriate? >> I expect because of the 'optionality' of attributes, at least in OM1. > > Aha! Having said which, it would be better to define a symbol rather than keep generating such lambda-expressions, if this applicatin were to go that way. James Davenport Visiting Full Professor, University of Waterloo Otherwise: Hebron & Medlock Professor of Information Technology and Chairman, Powerful Computing WP, University of Bath OpenMath Content Dictionary Editor and Programme Chair, OpenMath 2009 IMU Committee on Electronic Information and Communication _______________________________________________ Om mailing list [email protected] http://openmath.org/mailman/listinfo/om
