Hi,
if you want to use HOL Light, here is how it can be done.
Consider three boolean variable as follows:
pg means "portrait in Gold"
ig means "inscription on Gold is true"
is means "inscription on Silver is true"
Then you can compute the solution using rewriting with this command:
# REWRITE_CONV[PORTIA; EXISTS_BOOL_THM]
`?ig is. (ig <=> ~pg) /\ (is <=> (ig <=> ~is))`;;
val it : thm = |- (?ig is. (ig <=> ~pg) /\ (is <=> ig <=> ~is)) <=> pg
Marco
2018-06-26 19:55 GMT+02:00 Mario Xerxes Castelán Castro <
marioxcc...@yandex.com>:
> Hello. I am forwarding your message to the mailing list because you
> missed including it in your reply.
>
> > Perhaps the outer definition only needs to be
> > riddle is_in_gold ⇔
> > ...
>
> That is possible, of course:
> “““
> val riddle_def = Define‘
> riddle is_in_gold ⇔
> (∃gold_p silver_p.
> (gold_p ⇔ ¬is_in_gold) ∧
> (silver_p ⇔ (silver_p ⇎ gold_p)))’;
> ”””
> but this is harder to manipulate with automation tools as-is. For
> example, you could not easily pass it to the tactics based on a SAT
> solver because they do not handle existential quantifiers. You would
> ultimately 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 +0000
> From: Black, Paul E. (Fed) <paul.bl...@nist.gov>
> To: Mario Xerxes Castelán Castro <marioxcc...@yandex.com>
>
> Mario,
>
> An interesting solution! If I read it correctly, it requires too much
> from the solution. One only needs to determine which cask the pictures
> is in. One is not required to determine the truth or falsity of either
> inscription. Indeed, the inscription on the silver cask can be either
> true or false!
>
> Perhaps the outer definition only needs to be
> riddle is_in_gold ⇔
> ...
>
> -paul-
> Paul E. Black 100 Bureau Drive, Stop 8970
> paul.bl...@nist.gov Gaithersburg, Maryland 20899-8970
> voice: +1 301 975-4794 fax: +1 301 975-6097
> http://hissa.nist.gov/~black/
>
>
> ________________________________________
> From: Mario Xerxes Castelán Castro <marioxcc...@yandex.com>
> Sent: Tuesday, June 26, 2018 1:03 PM
> To: hol-info@lists.sourceforge.net
> Subject: Re: [Hol-info] Formalizing logical puzzles
>
> 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 a lot of puzzles, it may be worth doing
> automation. You can define a function that find the solution (if any)
> and then proves whether the solution is unique and a theorem with an
> explicit solution given.
>
> If you find this example useful please consider donating Bitcoins to
> 1F6zgVha3QwNqqpa7Wzf7cj52B7eyZSydX to help me with day to day running
> expenses.
>
>
>
> ------------------------------------------------------------
> ------------------
> 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
