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

Reply via email to