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.
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
