Hi Flemming and Micheal,
You both hit the nail on the head - I had a very basic syntax error (a
"school-boy error" if I ever saw one). I knew I'd made HOL Light prove it using
MESON beforehand and I didn't think that the new version of HOL would change
MESON that drastically!
Flemming, thank you for your quick overview of HOL Light - I now have a much
better understanding of how it goes about solving things. Also thank you for
pointing me towards the Examples folder - it contains a wealth of information
for my assignment.
Michael - yes, I think it should be ==> too. As Flemming has reminded me (I
should know - I am doing a course in Specification and Verification now, which
of course covers Logic), |- means syntactically derivable from.
Many thanks,
Nick Moore
-----Original Message-----
From: Andersen, Flemming L [mailto:[EMAIL PROTECTED]
Sent: Tue 15/04/2008 11:11 PM
To: MOORE N.G.
Cc: Harrison, John R
Subject: RE: [Hol-info] Predicate Logic Problem
Hi Nick,
You can write your own tactics in HOL Light (or HOL4) to verify all
kinds of properties and theorems. And since HOL is a polymorphic typed
Higher Order Logic based on Church type theory, you should be able to
specify and verify all kinds of mathematics in HOL since this was the
intension Chuch had when he defined his typ theory. But some things are
easy to specify and some are difficult.
In logic: A |- B usually means that if A |- B is valid given the
knowledge A we can syntactically derive B. And A |= B means that A
semantically implies B. If you want to read more about this, you can
study mathematics logic books like e.g.
Introduction to Mathematical Logic, Elliott Mendelson
You can also google: "mathematics logic" to get more information and
more books.
The problem that you have is that the HOL Light logic read a formula
like:
!x. P x /\ Q x |- (!x. P x) /\ (!x. Q x)
as
!x. ( P x /\ Q x |- (!x. P x) /\ (!x. Q x) )
and that is why you cannot prove it.
I guess that what you really mean is:
(!x. P x /\ Q x) |- (!x. P x) /\ (!x. Q x)
In HOL you can write and verify this as:
let QUANT_CONJ_lemma = TAC_PROOF
(([],
`!P Q. (!x:'a. P x /\ Q x) ==> ((!x. P x) /\ (!x. Q x))`),
REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC []
);;
Notice also that since we are dealing with Higher Order Logic, I have
explicitly quantified over P and Q so that you can specialize your lemma
into whatever predicate in x that you would like to be instantiated.
And if you want to look at examples on how all this and much more can be
done, there are some good examples in hol_light/Examples
I hope that this helps
Flemming
________________________________
From: [EMAIL PROTECTED]
[mailto:[EMAIL PROTECTED] On Behalf Of MOORE N.G.
Sent: Tuesday, April 15, 2008 9:19 AM
To: [email protected]
Subject: [Hol-info] Predicate Logic Problem
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
