2018-06-26 20:11 GMT+02:00 Marco Maggesi :
> # REWRITE_CONV[PORTIA; EXISTS_BOOL_THM]
> `?ig is. (ig <=> ~pg) /\ (is <=> (ig <=> ~is))`;;
>
> val it : thm = |- (?ig is. (ig <=> ~pg) /\ (is <=> ig <=> ~is)) <=> pg
>
Sorry, I made a mistake (thm PORTIA in the rewrite). Here is the
ltimately have to reformulate the problem to the form I used in my
first example.
Forwarded Message
Subject: Re: [Hol-info] Formalizing logical puzzles
Date: Tue, 26 Jun 2018 17:33:53 +
From: Black, Paul E. (Fed)
To: Mario Xerxes Castelán Castro
Mario,
An interesting solut
I made this theory script showing how you can use HOL4 to:
*Arrive at a solution of the riddle
*Then store a theorem with the solution
The theorem “riddle_solution” informally states that:
*The riddle has a solution.
*In any solution, the portrait is in the golden box.
If you are going to solve
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
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))
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
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 wrote:
>
> I’m working on learning the basics of using HOL to solve logic puzzles, such
> as the ‘Portia’s Suitor’ problem:
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
