Re: [isabelle] Destruction rule setup



On Sun, 12 Jul 2015, Larry Paulson wrote:

The original point of the setup was to create something that behaved like a sequent calculus. The two examples not included (not_conjD and imp_to_disjD) are redundant in this context, though for the former youâd need a detailed discussion of how negation is handled in order to see it. You could equally ask why impD is included as well as impCE, which is more general; the reason is that it handles an important special case well. It has to be admitted that there are many different ways of setting things up, and to find the best one would take a lot of experimentation. I did this in the 1990s (on largely first-order problems and set theory) but hardly at all since.

There is also a longer text by Larry from that time. Today it is section 9.4 "The Classical Reasoner" in the isar-ref manual.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.