Hi Dylan,
I'm familiar with HOL4 not HOL Light, but it looks as though they are
similar at this point: you have made a definition of a function called
goldInsc and you have named that definition (ie the theorem stating the
definition) goldInsc
Jeremy
On 06/27/2018 12:37 AM, Dylan Melville wrote:
Correcting a mistake: the goldInsc definition was supposed to be
# let goldInsc = new_definition `goldInsc gc <=> ~ gc`;;
On Jun 26, 2018, at 10:35 AM, Dylan Melville <dylanmelvi...@gmail.com
<mailto:dylanmelvi...@gmail.com>> wrote:
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
------------------------------------------------------------------------------
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
