Hello Dylan,
I think what you are looking for is new_axiom instead of new_definition.
Alternatively (and more conservatively), you can use your axioms as
assumptions in whatever (P) your are trying to prove:
g `(goldInsc gc <=> ~ gc) ==> (silvInsc gc <=> silvInsc gc <=> ~
(goldInsc gc)) ==> ... ==> P`;;
Hope this helps.
Regards,
Petros
On 26/06/2018 15:37, 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
--
Dr Petros Papapanagiotou
CISA, School of Informatics
The University of Edinburgh
Website: http://homepages.inf.ed.ac.uk/ppapapan/
Email: p...@ed.ac.uk
---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
------------------------------------------------------------------------------
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
