On Monday 16 May 2011 07:52, Mark wrote: > ? [rbj] > > Surely the ideal would be to avoid having ambiguous > > names by renaming as necessary? > > I would think so, yes. But I'm talking about the pretty > printer:
of course, I mistook the issue at stake. > given any internal representation of a theorem > (with whatever confusing forms of overloading that it > has), ensuring that the pretty printer output faithfully > represents that internal representation, so as not to > mislead the user. This is the pertinent question when it > comes to theorem prover trustworthiness (other than the > logical soundness of internal deductions and the > architecture of the inference kernel). Even though I am not particularly concerned with trustworthyness (at your level) it is still a awkwardness in my own use of ProofPower that I cannot get unambiguous and concise theory listings, partly because I get either too much or too little type information, or because of the effects of type abbreviations and aliasing. It sounds as if HOL4 and HOL zero have made some improvements in these areas. (I remember trying to learn HOL back in 1986 when HOL would not "invent" type variables and type checking came back with 1 bit of information (OK or not)). Roger Jones ------------------------------------------------------------------------------ Achieve unprecedented app performance and reliability What every C/C++ and Fortran developer should know. Learn how Intel has extended the reach of its next-generation tools to help boost performance applications - inlcuding clusters. http://p.sf.net/sfu/intel-dev2devmay _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
