Configurable search

[robblanco]

We have discussed briefly the convenience of a flexible search mechanism. In my prototypes, I am basically "monkey patching" an Abella session by importing code to steer an extended search tactic. However, I often use the same guidance code, and the act of importing is predictably brittle.

I think it should be possible for the user to configure how such an extended search will undergo its exploration, and for this a modicum of support from Abella would be beneficial (e.g., a command similar to Specification, possibly some namespace support).

What are your thoughts?

[lambdacalculator]

I'm not sure about how importing would affect search, but I've thought for a long time (and first suggested to Andrew in 2009) that it would be very useful to have a search with <HYP/THM NAMES> tactic that would include universally quantified hypotheses and/or theorems as backchain options during search. It shouldn't be very different from using program clauses, which are also universally quantified, during search; in effect, such hypotheses and theorems act as derived rules.

[chaudhuri]

Closing this since search with has been part of Abella for a while now. Feel free to comment if you think there is anything more to discuss on this particular issue.