Re: [Hol-info] On the wondering of detection of constructive proofs

[Marco M. <ma...@ma...>]

[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 <ai....@gm...>:

> 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 shu...@st...]
>
>
>
> ------------------------------------------------------------------------------
>
> _______________________________________________
> hol-info mailing list
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>