[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: How to kill a runaway proof attempt?

> Incidentally, I don't think there is anything wrong with trying commands
> like grind; if it doesn't terminate I simply do C-c C-c (restore), and if
> it terminates but isn't what I wanted to see (e.g., 140 subgoals) then I
> simply (undo).

There's lots of information on what (grind) and the other advanced
strategies do in CSL-95-10 "A less elementary tutorial for the PVS
specification and verification system". It also gives step by step
examples of it's use in proof development which could be useful.

The tech report is available on the web at:



Dave Stringer-Calvert, MEng MACM,  Department of Computer Science,
University of York, Heslington, York, YO1 5DD. [+44|0] 1904 432764