Great! This sounds easy to me :D
Thanks very much again!
Andrea
On 28/10/13 15:29, Ramana Kumar wrote:
To turn simplifier tracking on, just set the reference:
val _ = simpLib.track_rewrites := true
Then after some simplification, you can see what rewrites were used by
looking at
val result = !simpLib.used_rewrites
Alternatively, wrap your call to RW_TAC with simpLib.track, i.e. use
simpLib.track (RW_TAC [...]) [...]. Then examine the contents of
simpLib.used_rewrites as before.
P.S. Thanks Konrad, I didn't know about these before :)
On Mon, Oct 28, 2013 at 3:09 PM, Andrea <ag...@leicester.ac.uk
<mailto:ag...@leicester.ac.uk>> wrote:
Hi,
mmm.. I have not really understood how could I modify the flag.
The trial and error approach seems more feasible at my hol level.
However thank you both.
Bye,
Andrea
P.S: how do you understand which theorems helped in proofing your
goals when you use the RW_TAC reasoner?
On 25/10/13 23:45, Konrad Slind wrote:
There is a flag implemented so that the simplifier
tracks which rules are successfully applied. See
simpLib.{track,track_rewrites,used_rewrites}
Konrad.
On Fri, Oct 25, 2013 at 3:47 PM, Ramana Kumar
<ram...@member.fsf.org <mailto:ram...@member.fsf.org>> wrote:
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
<ag...@leicester.ac.uk <mailto:ag...@leicester.ac.uk>> 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
hol-info@lists.sourceforge.net
<mailto:hol-info@lists.sourceforge.net>
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
hol-info@lists.sourceforge.net
<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Android is increasing in popularity, but the open development platform that
developers love is also attractive to malware creators. Download this white
paper to learn more about secure code signing practices that can help keep
Android apps secure.
http://pubads.g.doubleclick.net/gampad/clk?id=65839951&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
