Hi Bill,
>MESON[]
>`(!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. P x y ==> P y x) /\
>(!x y. P x y \/ Q x y)
>==> (!x y. P x y) \/ (!x y. Q x y)`;;
>
>MESON solves this logic puzzle (which I still haven't yet
>solved) quite quickly, and it writes
>...solved at 23107
>
>let LosLogic_THM = thm `;
> let x y be A;
> let P Q be A->A->bool;
> assume ! x y z. P x y /\ P y z ==> P x z [H1];
> assume ! x y z. Q x y /\ Q y z ==> Q x z [H2];
> assume !x y. P x y ==> P y x [H3];
> assume !x y. P x y \/ Q x y [H4];
> thus (!x y. P x y) \/ (!x y. Q x y)
>
> proof
> qed by H1, H2, H3, H4`;;
>
>The miz3 proof is almost as quick, with a MESON `solved at'
>number of 23088.
Actually 23088 is _smaller_ than 23107, so I don't know
what you mean with "almost as quick" :-)
I have been trying to understand where the difference between
23107 and 23088 comes from. The reason is that MESON gets
as its argument a list of thms corresponding to H1 until H4,
instead of getting them as antecedents of an implication:
# MESON
[ASSUME `!x:A y:A z:A. P x y /\ P y z ==> P x z`;
ASSUME `!x:A y:A z:A. Q x y /\ Q y z ==> Q x z`;
ASSUME `!x:A y:A. P x y ==> P y x`;
ASSUME `!x:A y:A. P x y \/ Q x y`]
`(!x:A y:A. P x y) \/ (!x:A y:A. Q x y)`;;
0..0..2..7..16..30..48..72..108..168..236..340..516..702..918..1260..1660..2098..2716..3438..4298..5528..6944..8594..11052..13780..16742..20862..solved
at 23088val it : 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. P x y ==> P y x,
!x y. P x y \/ Q x y |- (!x y. P x y) \/ (!x y. Q x y)
#
So there's the 23088 again, see?
Freek
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
