Hi Rob, >Given a Z specification it could generate a set of proof >obligations called domain conditions. The idea was that >if the domain conditions were true, then the specification >was insensitive to the interpretation of undefined terms.
This is exactly what I was trying to describe, and the way things currently work in B as well, I think. (Of course B is very closely related to Z). >It ought to be feasible to do something similar for HOL. Ah, that sounds good! So I just am looking for a principled account of what a reasonable definition of those "domain conditions" are in the HOL logic. I think. Given that in HOL the logical connectives are defined in terms of more primitive notions like equality, you would like to have a calculus that gives you reasonable domain conditions for those logical connectives, based on how they are defined for terms that are just written in terms of equality. Freek ------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
