Email Gateway (Aug 18 2022 at 11:36): Email Gateway (Aug 18 2022 at 11:36):From: Jason Kirschenbaum <kirschenbaum.9@osu.edu>
Hi,
I'm trying to understand how to modify the classical reasoner to add
new rules. I'm pretty sure that the [intro], [elim] and [dest]
modifiers for theorems govern how the theorem will be used by the
reasoner. I'm having a hard time finding specific documentation on how
these modifiers work (include the differences between intro, and intro!
). If someone could point me to a document that would explain this, I
would really appreciated it.
Thanks in advance,
Jason
Email Gateway (Aug 18 2022 at 11:37):From: Lawrence Paulson <lp15@cam.ac.uk>
See Chapter 5 of the tutorial. To summarize:
intro denotes backward chaining, reducing goals to some goals.
dest denotes forward chaining, deducing a new assumption from an
assumption.
elim is a generalisation of dest; it can add multiple assumptions
and !!-variables.
The !-modifier gives the rule high priority and (like Prolog's cut)
prevents backtracking when that rule is chosen.
Larry
Last updated: May 03 2024 at 08:18 UTC