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»”.
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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
