There's no easy way to do this, that I know of, but there are several
difficult ways.
The simplest is: try removing the theorem from the list you give to
METIS_TAC (or RW_TAC) and see if the proof still goes through or not.
This is a trial and error approach, so is a bit tedious, but is at least
simple.
The other approaches I can think of would involve proof recording of some
kind: possibly using the OpenTheory logging kernel, or some custom-made
proof-logging code, then inspecting the proof of the theorem to see which
other theorems it references.
On Fri, Oct 25, 2013 at 3:25 PM, Andrea <[email protected]> wrote:
> Hi everyone,
>
> I am advancing step by step in the tutorial, and now I am interactively
> following the example of the Euclid's theorem proofing.
> In this example it is made an heavy usage of the MATIS_TAC reasoner, and
> here my question: is it possible to see which theorem the reasoner
> chooses among those given in the list?
> I think it would help me in understanding how the proof is built.
> Thank you anyway,
>
> Andrea
>
>
> ------------------------------------------------------------------------------
> October Webinars: Code for Performance
> Free Intel webinars can help you accelerate application performance.
> Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most
> from
> the latest Intel processors and coprocessors. See abstracts and register >
> http://pubads.g.doubleclick.net/gampad/clk?id=60135991&iu=/4140/ostg.clktrk
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
October Webinars: Code for Performance
Free Intel webinars can help you accelerate application performance.
Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from
the latest Intel processors and coprocessors. See abstracts and register >
http://pubads.g.doubleclick.net/gampad/clk?id=60135991&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
