Hi Robert, It is easy to answer this question for the OpenTheory standard theory library by using this command:
opentheory info --theory --show-assumptions --show-derivations base For each theorem this displays which of the three axioms (Extensionality, Choice and Infinity) it depends on. Cheers, Joe On Mon, Jun 8, 2015 at 10:40 AM, Robert White <[email protected]> wrote: > 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 (Shuai Wang) > INRIA 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
