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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
