Hi John,
I've just realised HOL light has a prover9 interface! It has very impressive
performance. I have a couple of questions.
----------
I have a problem running the following example:
let reflexive_def = new_definition `
reflexive R X = ! x. X x ==> R x x
`;;
let transitive_def = new_definition `
transitive R X = ! x y z. X x /\ X y /\ X z ==> R x y /\ R y z ==> R x z
`;;
let anti_def = new_definition `
anti R X = ! x y. X x /\ X y ==> R x y /\ R y x ==> (y=x)
`;;
let total_def = new_definition `
total R X = ! x y. X x /\ X y ==> (R x y \/ R y x)
`;;
let linear_def = new_definition `
linear R X = (reflexive R X /\ transitive R X /\ anti R X /\ total R X)
`;;
let t = `
(! R'.
(! X Y Z W.
(! x. D x = (X x \/ Y x \/ Z x \/ W x))
/\ (! x. ((X x /\ Y x) \/ (X x /\ Z x) \/ (X x /\ W x) \/ (Y x /\ Z x) \/ (Y
x /\ W x) \/ (Z x /\ W x)) ==> F)
/\ linear R D
/\ (! x y. X x /\ Y y ==> R x y)
/\ (! y z. Y y /\ Z z ==> R y z)
/\ (! z w. Z z /\ W w ==> R z w)
/\ (! x y. R' x y = ((R x y /\ ~ (Y x /\ Z y)) \/ (Z x /\ Y y)))
==> linear R' D))
`;;
let t2 = (snd o dest_eq o concl)
(REWRITE_CONV[reflexive_def;transitive_def;anti_def;total_def;linear_def]
t);;
let _ = time PROVER9 t2;;
The output I get is
-------- Proof 1 --------
THEOREM PROVED
------ process 7980 exit (max_proofs) ------
Failed after (user) CPU time of 2.831569: Exception: Failure "find".
where I presume it is failing to find the "F" clause in the proof
reconstruction phase. Do you have any idea what the problem might be?
-------------
Related to this example, I have a question about the standard options in
file prover9.ml:
let prover9_options = ref
("clear(auto_inference).\n"^
"clear(auto_denials).\n"^
"clear(auto_limits).\n"^
"set(neg_binary_resolution).\n"^
"set(binary_resolution).\n"^
"set(paramodulation).\n");;
If I run with these options prover9 takes a long time, but if I run with the
default prover9 settings (by modifying the prover9.ml file), prover9 proves
the goal very quickly. However, I suspect that it may only be proving a
single disjunct rather than all the disjuncts (?). Can you confirm this?
Thanks
Tom
-------------------------------------------------------------------------
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
