Juan Perna wrote: > Hello, > > I am needing to transform a goal of the form: "?x.!y. (P x y)" into > "!y.?x. (P x y)" but I haven't been able to find anything like that in > the "bool" theory (or anywhere else). I looked for it using: > > DB.match ["-"] ``!P. (!x.?y. P) ==> (?y.!x. P)``; > DB.match [] ... gives the same result. I would have probably searched with a slightly more general expression, something like
DB.match [] ``?y. !x. P x y`` but it's a matter of taste. This will find SKOLEM_THM which is related to what you want ... > but this didn't bring any results. > > On the other hand, I know it is true that: > > ?x.!y. (P x y) ==> !y.?x. (P x y) > > (which is what I need). > You can prove this with METIS_PROVE: - METIS_PROVE [] ``(?x.!y. (P x y)) ==> !y.?x. (P x y)``; <<HOL message: inventing new type variable names: 'a, 'b>> metis: r[+0+3]# > val it = |- (?x. !y. P x y) ==> !y. ?x. P x y : thm but you won't be able to apply it to advance your goal. The implication is going the wrong way. And the other direction isn't valid (consider < on the integers). > How do I look for this kind of > rules/conversions in the existing theories? > Most of the basics having to do with boolean structure and quantifiers is already proved in boolTheory. So you can find it there using DB.match. Or you can attempt to prove such things on the fly, using DECIDE or METIS_PROVE (using decision procedures as a kind of database lookup). Konrad. ------------------------------------------------------------------------- This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2005. http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
