Good afternoon,
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?
Confusingly, I am quite sure I have managed to get HOL Light to prove it the
above way previously, however I recently upgraded my version of Ocaml to 3.10.0
and thus have moved to the development branch on HOL Light - could this be
causing the problem?
Many thanks for any help,
Nick Moore
-------------------------------------------------------------------------
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
