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
