[I forgot to replay to the list ...] Hi Robert,
in HOL Light you can use ITAUT (or ITAUT_TAC). The documentation (https://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/ITAUT.html) says: Normally, first-order reasoning should be performed by MESON[], which is much more powerful, complete for all classical logic, and handles equality. The function ITAUT is mainly for ``bootstrapping'' purposes. Nevertheless it may sometimes be intellectually interesting to see that certain logical formulas are provable intuitionistically. 2015-06-08 19:40 GMT+02:00 Robert White <[email protected]>: > Dear all, > > I wonder how I can detect if there law of excluded middle or double > negation elimination used in a proof. Basically, I am trying to find out if > a proof is classical or constructive. > > Since when I use TAUT or other rewriting functions I won't get a direct > idea if it is classical or constructive. I wonder if there is anyway I can > find out. > > Thanks a lot. > > -- > > Regards, > Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang) > INRIA Deducteam <https://www.rocq.inria.fr/deducteam/> > [Moving to ILLC of UvA from this Sep. ] > [New email address will be [email protected]] > > > > ------------------------------------------------------------------------------ > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
