search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Configurable search #93

Closed robblanco closed 10 months ago

robblanco commented 7 years ago

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 commented 7 years ago

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 commented 10 months ago

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.