Hi Nick,
I think Flemming and Michael have more or less answered your question,
but here's a bit more detail.
| 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).
HOL Light's MESON/MESON_TAC that you tried implements a form of model
elimination that is complete for first-order logic with equality. In
principle, this gives the same power as prover9. In practice it isn't
even in the same league on difficult problems, especially those
requiring non-trivial equational reasoning. On the other hand, HOL
Light has some theory-specific automation for arithmetic and algebra
that prover9 lacks (ARITH_RULE, REAL_FIELD etc.) together with more
general programmability and the fact that all proof proceeds via a
small trusted core.
Perhaps it isn't directly relevant to your project, but I became so
keen on prover9 last summer that I wrote a HOL Light interface to it,
which calls prover9 on a HOL problem, parses back the proof and uses
it to construct a primitive inference trail. A few examples can be
found appended at the end of this message. The source code is in
"Examples/prover9.ml" in the development snapshot.
| 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
| "<=>"?
HOL Light uses "|-" as a meta-notion "is provable", and it can't be
entered directly as a term/formula. However the underlying semantics
is essentially the same as implication "==>", and you can convert
a theorem "|- p ==> q" into "p |- q" using UNDISCH. Thus your problem
could be solved like this:
# MESON[] `(!x. P x /\ Q x) ==> (!x. P x) /\ (!x. Q x)`;;
Warning: inventing type variables
val it : thm = |- (!x. P x /\ Q x) ==> (!x. P x) /\ (!x. Q x)
# UNDISCH it;;
val it : thm = !x. P x /\ Q x |- (!x. P x) /\ (!x. Q x)
In fact the version with "<=>" should work too; I suspect your
problem may simply have been a question of operator precendence
etc. Note that the scope of quantifiers extends as far to the
right as possible so the following works:
# MESON[] `(!x. P x /\ Q x) <=> (!x. P x) /\ (!x. Q x)`;;
Warning: inventing type variables
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
val it : thm = |- (!x. P x /\ Q x) <=> (!x. P x) /\ (!x. Q x)
but this does not:
# MESON[] `!x. P x /\ Q x <=> (!x. P x) /\ (!x. Q x)`;;
Warning: inventing type variables
0..0..1..2..3..4..5..6..7..8..9..10..11..12..13..14..15..16..17..18..1
9..20..21..22..23..24..25..26..27..28..29..30..31..32..33..34..35..36.
.37..38..39..40..41..42..43..44..45..46..47..48..49..Exception:
Failure "solve_goal: Too deep".
This scoping rule is typical these days, but is the opposite of the
convention in many of the classic logic texts (Enderton, Mendelson
etc.) and is a common source of confusion.
John.
******* Prover9 interface examples *******
# let LOS = PROVER9
`(!x y z. P(x,y) /\ P(y,z) ==> P(x,z)) /\
(!x y z. Q(x,y) /\ Q(y,z) ==> Q(x,z)) /\
(!x y. Q(x,y) ==> Q(y,x)) /\
(!x y. P(x,y) \/ Q(x,y))
==> (!x y. P(x,y)) \/ (!x y. Q(x,y))`;;
Warning: inventing type variables
-------- Proof 1 --------
THEOREM PROVED
------ process 10820 exit (max_proofs) ------
val ( LOS ) : thm =
|- (!x y z. P (x,y) /\ P (y,z) ==> P (x,z)) /\
(!x y z. Q (x,y) /\ Q (y,z) ==> Q (x,z)) /\
(!x y. Q (x,y) ==> Q (y,x)) /\
(!x y. P (x,y) \/ Q (x,y))
==> (!x y. P (x,y)) \/ (!x y. Q (x,y))
# let CONWAY_2 = PROVER9
`(!x. 0 + x = x) /\
(!x y. x + y = y + x) /\
(!x y z. x + (y + z) = (x + y) + z) /\
(!x. 1 * x = x) /\ (!x. x * 1 = x) /\
(!x y z. x * (y * z) = (x * y) * z) /\
(!x. 0 * x = 0) /\ (!x. x * 0 = 0) /\
(!x y z. x * (y + z) = (x * y) + (x * z)) /\
(!x y z. (x + y) * z = (x * z) + (y * z)) /\
(!x y. star(x * y) = 1 + x * star(y * x) * y) /\
(!x y. star(x + y) = star(star(x) * y) * star(x))
==> !a. star(star(star(star(a)))) = star(star(star(a)))`;;
-------- Proof 1 --------
THEOREM PROVED
------ process 13344 exit (max_proofs) ------
val ( CONWAY_2 ) : thm =
|- (!x. 0 + x = x) /\
(!x y. x + y = y + x) /\
(!x y z. x + y + z = (x + y) + z) /\
(!x. 1 * x = x) /\
(!x. x * 1 = x) /\
(!x y z. x * y * z = (x * y) * z) /\
(!x. 0 * x = 0) /\
(!x. x * 0 = 0) /\
(!x y z. x * (y + z) = x * y + x * z) /\
(!x y z. (x + y) * z = x * z + y * z) /\
(!x y. star (x * y) = 1 + x * star (y * x) * y) /\
(!x y. star (x + y) = star (star x * y) * star x)
==> (!a. star (star (star (star a))) = star (star (star a)))
# let DOUBLE_DISTRIB = PROVER9
`(!x y z. (x * y) * z = (x * z) * (y * z)) /\
(!x y z. z * (x * y) = (z * x) * (z * y))
==> !a b c. (a * b) * (c * a) = (a * c) * (b * a)`;;
-------- Proof 1 --------
THEOREM PROVED
------ process 11516 exit (max_proofs) ------
val ( DOUBLE_DISTRIB ) : thm =
|- (!x y z. (x * y) * z = (x * z) * y * z) /\
(!x y z. z * x * y = (z * x) * z * y)
==> (!a b c. (a * b) * c * a = (a * c) * b * a)
-------------------------------------------------------------------------
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
