Hi Bill,
| The error at the end is
|
| ::#2
| :: 2: inference time-out
| `,
| (0, 1, 0)).
This is a genuine inference timeout, which does indeed seem surprising
for such a simple problem. You did a good job of boiling down the
essential core. To extract it from miz3 completely, the goal to be
proved is effectively:
`(Between (a,b,x) \/ Between (a,x,b) \/ Between (x,a,b)) /\
(Between (a,b,c) \/ Between (a,c,b) \/ Between (c,a,b))
==> Between (a,b,x) /\ Between (a,b,c) \/
Between (a,b,x) /\ Between (a,c,b) \/
Between (a,b,x) /\ Between (c,a,b) \/
Between (a,x,b) /\ Between (a,b,c) \/
Between (a,x,b) /\ Between (a,c,b) \/
Between (a,x,b) /\ Between (c,a,b) \/
Between (x,a,b) /\ Between (a,b,c) \/
Between (x,a,b) /\ Between (a,c,b) \/
Between (x,a,b) /\ Between (c,a,b)`;;
This can be solved trivially with the right tactic, but the default
provers used in miz3 (HOL_BY and MESON) perform case splitting
somewhat overenthusiastically, as a result of which they take an
significant fraction of a second. This is enough to overstep the low
default inference timeout in miz3. There are two quick fixes:
1. Use a specific tactic that will solve the goal faster, e.g.
replace the final line with
qed by CONV_TAC TAUT, X1, X2
2. Increase the default inference timeout for miz3. This will make
the built-in provers effectively more powerful, but will slow
down the rejection of faulty proofs, making debugging slower.
reset_miz3 0; timeout := 5;;
Anyway, since neither of these is entirely satisfying, I will take a
look at the default prover implementation to see if it can do a
better job in such situations. Naturally, you could also consider
buying a machine with a new and faster processor :-)
John.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
