Dear Vincent, >I see. I'll have a look for my culture, but I think in the end that it > will be simpler, if I need it, to just translate my current HINT_EXISTS_TAC to > HOL4 (roughly nothing more than Ocaml->SML). I'll have a look at > quantHeuristicsLib when I get the time though, because maybe the > my problem will actually happen to be useless in the end.
this makes sense. Using quantHeuristicsLib or consequence conversions would provide you with a bit more power. However, to solve exactly the problem you described, it is really easier to just port your OCaml code. I might be interested in your problem in general, though. I still look for users for my quantifier heuristic library. I implemented this library as an extensible one than can easily be extended by the user. What kind of quantifier problems do you have? Is there some other kind of automation you might be interested in. Best Thomas On Fri, 2012-12-28 at 07:18 -0500, Vincent Aravantinos wrote: > Hi Thomas, > > Le 27/12/12 07:30, Thomas Tuerk a écrit : > > On Thu, 2012-12-27 at 19:55 +0800, Ramana Kumar wrote: > >> There might be something in quantHeuristicsLib that can help, but I'm > >> not sure. > > quantHeuristicsLib can do it (see below), but has other restrictions. > > > > SATISFY_ss allows to instantiate multiple variables at the same time. > > So, it can for example handle: > > > > ?x y. P x y /\ Q y x > > --------------------- > > 0. P 1 2 > > 1. !x. Q 2 x > > > > Notice, assumption 1. SATISFY_ss does not use matching but unification > > with restriction to the variables occurring all-quantified > > in an assumption or existentially in the current goal. > > quantHeuristicsLib can currently only handle one variable at a time. > I thought of this problem (handling more than 1 variable at a time) while > writing HINT_EXISTS_TAC but came to the conclusion that I just wanted > a pragmatic solution that does not claim to solve all the problems but > just to be useful in many situations. Therefore, solving for one variable > only seemed sufficient to me. > > > However, using consequence conversions it can do your kind of > > instantiation guessing also at subpositions. > > > > Getting quantHeuristicLib to do what you want requires writing some > > ML-code, though. By default, it only searches for guesses with > > justification, i.e. it only instantiates a quantifier, if it can > > prove that the resulting term is really equivalent. > > For example: > > > > ?x. P x /\ Q x > > ------------------- > > P 2 > > > > would not be instantated with 2, because Q 2 might be false, but there > > may still be a "x" that satisfies both. In order to get it working for > > your case, you need to "tell" it to use unjustified guesses for > > conjunction. Given ?x. X x /\ Y x, it should search for guesses for X x > > and Y x and return all found guesses, even if it can't prove that they > > are not guesses for the overall conjunct. > > > > "implication_concl_qp" in > > "src/quantHeuristicsLib/quantHeuristicsParameter" does this for the > > right hand side of implications. One could use that code as a basis or > > generalise it. > I see. I'll have a look for my culture, but I think in the end that it > will be > simpler, if I need it, to just translate my current HINT_EXISTS_TAC to > HOL4 (roughly nothing more than Ocaml->SML). I'll have a look at > quantHeuristicsLib when I get the time though, because maybe the > my problem will actually happen to be useless in the end. > > Thanks, > V. > ------------------------------------------------------------------------------ Master SQL Server Development, Administration, T-SQL, SSAS, SSIS, SSRS and more. Get SQL Server skills now (including 2012) with LearnDevNow - 200+ hours of step-by-step video tutorials by Microsoft MVPs and experts. SALE $99.99 this month only - learn more at: http://p.sf.net/sfu/learnmore_122512 _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
