I am replying assuming HOL4. Loosely speaking, definitions should be used only for objects that you can describe in terms of other objects already defined. For riddles, you should formulate the problem as a system of boolean equations, then you can prove that it has a unique solution. For convenience, you can give the system of equations a name, that is, employ it as the right hand side of a definition.
On 26/06/18 09:35, Dylan Melville 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 >
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
