Hello again,
I understand that HOL is a reasoner for classical logic so there is no
surprise when I want to prove something using rewriting I get a set of
rules as basic_rewrites where we can find ~ ~t <=> t; there.
So here comes the question, is there a way we can get intuitionistic set or
rewriting rules in HOL Light already to do pure constructive logic
reasoning?
Thanks again.
--
Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
