Re: [Hol-info] Formalizing logical puzzles

2018-06-26 Thread Marco Maggesi 
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
corrected version:

# REWRITE_CONV[EXISTS_BOOL_THM]
​​
`?ig is. (ig <=> ~pg) /\ (is <=> (ig <=> ~is))`;;

val it : thm = |- (?ig is. (ig <=> ~pg) /\ (is <=> ig <=> ~is)) <=> pg
​
--
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

Re: [Hol-info] Formalizing logical puzzles

2018-06-26 Thread Mario Xerxes Castelán Castro 
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 +
From: Black, Paul E. (Fed) 
To: Mario Xerxes Castelán Castro 

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-4794fax: +1 301 975-6097
http://hissa.nist.gov/~black/



From: Mario Xerxes Castelán Castro 
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.




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

Re: [Hol-info] Formalizing logical puzzles

2018-06-26 Thread Mario Xerxes Castelán Castro 
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.



riddleScript.sml
Description: application/smil


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

Re: [Hol-info] Formalizing logical puzzles

2018-06-26 Thread Mario Xerxes Castelán Castro 
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

Re: [Hol-info] Formalizing logical puzzles

2018-06-26 Thread Petros Papapanagiotou 

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 > 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

Re: [Hol-info] Formalizing logical puzzles

2018-06-26 Thread Jeremy Dawson 

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 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 > 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



--
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

Re: [Hol-info] Formalizing logical puzzles

2018-06-26 Thread 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:
> 
> 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

[Hol-info] Formalizing logical puzzles

2018-06-26 Thread Dylan Melville 
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