Hi,
just too clarify. Axioms and oracles are different things in HOL 4. In
the context of HOL 4, an "oracle" usually refers to external proof tool
which is trusted by HOL. Its results are "imported" using HOL's "oracle
mechanism" (mk_oracle_thm and related). Oracles are __not__ axiom
schemata. Axioms are only used to make your logic stronger, i.e. (2). Of
course, in a theorem prover you can abuse axioms to do (1). However,
even if you do it, you would not call it introducing new axioms.
However, usually theorem provers provide a different mechanism for (1).
In HOL 4 the oracle mechanism is used for (1). Things like
"boosLib.cheat" are implemented with it.
Best
Thomas
On 12.03.2018 18:41, Mario Xerxes Castelán Castro wrote:
> There are 2 reasons for adding new axioms and axiom schemata (oracles):
>
> (1) To save the work for proving something provable or constructible
> (e.g.: one could assume the axioms for the real numbers instead of
> constructing the reals; although in this case, the library includes a
> construction of the reals)
>
> (2) Because the axiom is not provable from within the logic, i.e.: you
> want to make the theory stronger.
>
> In case (1), maybe the axiom you needs are already proved or available
> as a theory. You will have to search for it. Check the theory tree
>
> In case (2), you can add a new axiom (refer to Thomas message) or state
> your theorems as an implication, where the antecedent suffices to encode
> your new axioms or axiom schemata.
>
>
>
> ------------------------------------------------------------------------------
> 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
------------------------------------------------------------------------------
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
