Re: [Hol-info] HOL Help for Axiom.
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
Re: [Hol-info] HOL Help for Axiom.
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. Michael From: Thomas Tuerk Date: Tuesday, 13 March 2018 at 08:51 To: "hol-info@lists.sourceforge.net" Subject: Re: [Hol-info] HOL Help for Axiom. 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<mailto: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
Re: [Hol-info] HOL Help for Axiom.
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
Re: [Hol-info] HOL Help for Axiom.
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
Re: [Hol-info] HOL Help for Axiom.
Dear Sana, it is easily possible to define own axioms and inference rules. However, it very easily leads to inconsistencies and is usually not advisable expect if you really know what you are doing. In most cases the definitional extension principles provided by HOL suffice and are much safer to use (see https://hol-theorem-prover.org/hol-course.pdf, slide 121 onwards). HOL distinguishes between new axioms (https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/Docfiles/HTML/Theory.new_axiom.html) and oracles (https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/Docfiles/HTML/Thm.mk_oracle_thm.html). "new_axiom" and "mk_oracle_thm" both introduce new theorems without requiring a proof. They are therefore very similar. However, "new_axiom" is intended to be used for extending the logic of HOL, while "mk_oracle_thm" is used to introduce theorems that could be proved in the existing logic but for which you don't have a proof. A typical example is that you trust the results of some oracle like an external sat solver. From a pragmatic point of view, it is hard to keep track of what depends on a new axiom, while it is thanks to tags easy to keep track of what depends on an oracle theorem. New inference rules can be coded as ML functions using "mk_oracle_thm". So, it is easy to define own inference rules and axioms. However, it is usually not necessary. You can introduce inconsistencies when doing it and might have a harder time convincing reviewers that your development is sensible. I would therefore check double, whether tools like "new_specification" (https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/Docfiles/HTML/Definition.new_specification.html) are not more useful for your purposes. Best Thomas On 12.03.2018 08:54, Sana Imtiaz via hol-info wrote: > Hey. > Hope you are fine. I am doing MS from National University of Science > and Technology Islamabad. I need your help as i am working with HOL > environment. Is it possible to define an *Inference Rule* or *Axiom* > by myself? Kindly please guide me in this matter. > > Waiting for your kind response. Thank you. > > Regards, > Sana Imtiaz > MSIT-16 > NUST > > > -- > 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
