On Tue, 24 Apr 2012, Bill Richter wrote:
> Roger, if there's ``some cultural aversion to the use of axioms in the
> HOL community,'' then maybe HOL isn't the right proof-checker to use in
> high school geometry classes. Does anyone think there is a better
> proof-checker? My guess is that this is just an interface problem that
> HOL could easily solve, and I'm willing to work on it myself.
The strict definitional approach is mainly for foundational purposes, and
for good reasons. The HOL community usually quotes Bertrand Russel on
that:
The method of "postulating" what we want has many advantages; they are
the same as the advantages of theft over honest toil.
Introduction to Mathematical Philosophy, New York and London, 1919, p 71.
This means things like inductive definitions, datatypes, recursive
functions are explicitly reduced to basic principles, not "axiomatized" by
some magic ML code. Moreover your own concepts should be defined
properly, and results stated and proven explicitly.
Nonetheless, this does not prevent the user from working in a local
context with parameters and assumptions in a quasi-axiomatic manner.
Your results would then be releative to certain premises my_pred x y z ==>
... in terms of the logical foundations. By organizing such assumptions
in a reasonable way, your application does not have to expose this to the
end-user.
Don't ask me how to do that in HOL4, HOL-Light, ... though. I am merely a
guest on this mailing list.
Makarius
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
