I’m working on learning the basics of using HOL to solve logic puzzles, such as
the ‘Portia’s Suitor’ problem:
Portia has a gold casket and a silver casket and has placed a picture of
herself in one of them. On the caskets, she has written the following
inscriptions:
• Gold: The portrait is not in here
• Silver: Exactly one of these inscriptions is true.
Portia explains to her suitor that each inscription may be true or false, but
that she has placed her portrait in one of the caskets in a manner that is
consistent with the truth or falsity of the inscriptions.
If the suitor can choose the casket with her portrait, she will marry him.
Obviously this is a very simple problem, but when inputting the proof into HOL
Light, I had an issue. The first axiom, the gold inscription I formalized as
# let goldInsc = new_definition `goldInsc gc = not gc`;;
Then attempted the silver inscription as
# let silvInsc = new_definition `silvInsc gc <=> silvInsc gc <=> ~ (goldInsc
gc)`;;
Which doesn’t work as intended, obviously since goldInsc is a theorem, not an
actual function. What is the proper way to express the silver inscription?------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
