On 12/03/18 16:24, michael.norr...@data61.csiro.au wrote:
> Indeed.  There is no need to distinguish axioms and axiom schemata (as Thomas 
> said, oracles are not the latter). This is because of the INST and INST_TYPE 
> rules of inference.  In a system with schemata, instantiation (or matching) 
> is the way you check whether or not you have an oracle, and you have a 
> special category of schema variable. The variables in HOL’s axioms are normal 
> variables, and can be instantiated both in axioms and derived theorems.

I welcome the clarification, because it may be confusing for people who
read my message without context, but I am aware of the difference. By
axiom schema I do not mean instantiations of boolean functions (which of
course, is expressible in-logic within HOL). What I mean is that an
oracle is (usually) an axiom schema of the form «P» with side condition
“SMT solver X or decision procedure Y yields «P»”.

Attachment: signature.asc
Description: OpenPGP digital signature

Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
hol-info mailing list

Reply via email to