On Mon, May 21, 2012 at 3:29 AM, Lu Zhao luz...@cs.utah.edu wrote:
This is particularly dangerous when I have proof automation scripts that
try different rewriting rules. The number reported is not representative
on the complexity of the problem, but the number of inference steps
conducted by
Ramana Kumar wrote:
On Mon, May 21, 2012 at 3:29 AM, Lu Zhao luz...@cs.utah.edu wrote:
This is particularly dangerous when I have proof automation scripts that
try different rewriting rules. The number reported is not representative
on the complexity of the problem, but the number of
Using the following method has some problems, when there are failures in
proof attempts. For example, the following sequence reports 44 primitive
inference steps, after a proof failure.
val meter = Count.mk_meter();
g `p /\ p /\ q /\ F`;
e (METIS_TAC []);
Count.report(Count.read meter);
This
This is certainly true. Of course, it all depends on what you're trying to
measure. If you're interested in the size of the natural deduction proof that
actually establishes a particular theorem, you really need to try something
like: extracting the proof using some sort of recording
Thanks Lu! And thanks for Dr. Michael Norrish!
Sorry I'm not familiar with Structure Count. Now, I got it!
Best Wishes,
Liya
Quoting Michael Norrish michael.norr...@nicta.com.au:
On 07/04/11 14:19, Lu Zhao wrote:
First, please forgive me if this question is too silly. I had this
question
On Thursday 07 April 2011 02:07:11 am Michael Norrish wrote:
On 07/04/11 14:19, Lu Zhao wrote:
First, please forgive me if this question is too silly. I had this
question when I talked to a colleague, who has no idea about theorem
proving at all, about the amount of proof work that can be
