> Ok, so if I understand this correctly the validity checks are only in > place to keep you from going down an inference chain that is guarenteed > to go no where in making progress towards proving your goal. This being > only an issue when searching for the proof itself in the interactive > prompt, not when just verifying it.
The way I think about it is that the validity check makes sure that no assumptions beyond those stated in the goal enter the proof. For some applications, adding new assumptions might be just the trick, e.g., when exploring a proof to see what assumptions are needed. In that case, expandf is your friend. Konrad. ------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_sfd2d_oct _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
