MOORE N.G. wrote: > I'm a student at Durham University who's currently doing a small > research project on HOL Light (on it's basic capabilities and > comparing it to a fully automated proof system - in my case I'm > comparing it to Prover9).
> The root of my problem is that we have to demonstrate whether or not > HOL Light can prove the following expression (converted into HOL > Light syntax for simplicity): > !x. P x /\ Q x |- (!x. P x) /\ (!x. Q x) > Firstly, how does one represent "|-" in HOL Light? Is it equivalent > to "<=>"? > Secondly, which rule would solve this? I have tried using MESON[] > (and replacing "|-" with "<=>"), however this did not work. Or can't > HOL Light solve problems in this way and have I mis-understood the > limitations of HOL Light? I imagine that you may have unwittingly asked the system to prove !x. (P x /\ Q x <=> (!x. P x) /\ (!x. Q x)) If you try (!x. P x /\ Q x) <=> (!x. P x) /\ (!x. Q x) MESON should prove it (it certainly does on HOL4). Incidentally, without knowing what prover9's syntax is, I'm afraid I have no idea what |- is supposed to mean. However, it rather looks as if you should be using implication rather than bi-implication: (!x. P x /\ Q x) ==> (!x. P x) /\ (!x. Q x) Michael. ------------------------------------------------------------------------- This SF.net email is sponsored by the 2008 JavaOne(SM) Conference Don't miss this year's exciting event. There's still time to save $100. Use priority code J8TL2D2. http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
