Re: [isabelle] any way to increase force search depth?



I assume that by UI you mean universal instantiation. Isabelle instantiates quantifiers solely by unification. It could be interesting to investigate whether some proofs would benefit from automated explicit substitution of candidate terms.

As Jeremy mentioned, at the ML level Isabelle provides a flexible tactic language in which you can express various search strategies that may be able to automate your proofs, and there are ways of inserting ML tactics into Isar proofs or encapsulating them as Isar methods.

Larry Paulson


On 1 Jun 2010, at 01:00, Andrei Borac wrote:

> So, my speculation at this point is that force does not blindly try
> UIs, but looks for some correlation between the stuff in the UI and
> the other facts in the assumption block. What I am thinking is the
> best option at this point is to write some kind of control program
> that will interact with Isabelle, first inserting the thy file up the
> current point and then try all possible (type-sane) instantiations
> followed by force until one succeeds ... after a long time, I will
> have a long script that can be cut & paste into the thy file ...






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