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> 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
