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) <[email protected]>
To: Mario Xerxes Castelán Castro <[email protected]>
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
[email protected] 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 <[email protected]>
Sent: Tuesday, June 26, 2018 1:03 PM
To: [email protected]
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.
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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
