Cheryl's Birthday - Revision history

Michael Leuschel at 09:22, 18 April 2015

2015-04-18T09:22:07Z

← Older revision		Revision as of 09:22, 18 April 2015
Line 6:		Line 6:

	In case you are new to B, you probably need to know the following operators to understand the specification below (we als have a [[Summary_of_B_Syntax\|summary page about the B syntax]]):		In case you are new to B, you probably need to know the following operators to understand the specification below (we als have a [[Summary_of_B_Syntax\|summary page about the B syntax]]):
	* <tt>x : S</tt> specifies that x is an element of S		* <tt>x : S</tt> specifies that x is an element of S
	* <tt>dom(r)</tt> is the domain of a function or relation		* <tt>dom(r)</tt> is the domain of a function or relation r
	* <tt>r~</tt> is the inverse of a function or relation		* <tt>r~</tt> is the inverse of a function or relation r
	* <tt>r[S]</tt> is the relational image of a relation r for a set of domain values S		* <tt>r[S]</tt> is the relational image of a relation r for a set of domain values S
	* <tt>card(S)</tt> is the cardinality of a set		* <tt>card(S)</tt> is the cardinality of a set S
	* <tt>a\|->b</tt> represents the pair (a,b); note that a relation and function in B is a set of pairs.		* <tt>a\|->b</tt> represents the pair (a,b); note that a relation and function in B is a set of pairs.
	* <tt>!x.(P => Q)</tt> denotes universal quantification over variable x		* <tt>!x.(P => Q)</tt> denotes universal quantification over variable x

	<pre>		<pre>

Michael Leuschel at 09:21, 18 April 2015

2015-04-18T09:21:29Z

← Older revision		Revision as of 09:21, 18 April 2015
Line 6:		Line 6:

	In case you are new to B, you probably need to know the following operators to understand the specification below (we als have a [[Summary_of_B_Syntax\|summary page about the B syntax]]):		In case you are new to B, you probably need to know the following operators to understand the specification below (we als have a [[Summary_of_B_Syntax\|summary page about the B syntax]]):
	* <tt>x : S<tt> specifies that x is an element of S		* <tt>x : S</tt> specifies that x is an element of S
	* <tt>dom(r)</tt> is the domain of a function or relation		* <tt>dom(r)</tt> is the domain of a function or relation
	* <tt>r~</tt> is the inverse of a function or relation		* <tt>r~</tt> is the inverse of a function or relation

Michael Leuschel at 09:06, 18 April 2015

2015-04-18T09:06:21Z

← Older revision		Revision as of 09:06, 18 April 2015
Line 12:		Line 12:
	* <tt>card(S)</tt> is the cardinality of a set		* <tt>card(S)</tt> is the cardinality of a set
	* <tt>a\|->b</tt> represents the pair (a,b); note that a relation and function in B is a set of pairs.		* <tt>a\|->b</tt> represents the pair (a,b); note that a relation and function in B is a set of pairs.
	* <tt>!x.(P => Q)</tt> denotes universal quantification over variable x		* <tt>!x.(P => Q)</tt> denotes universal quantification over variable x

	<pre>		<pre>

Michael Leuschel at 09:04, 18 April 2015

2015-04-18T09:04:59Z

← Older revision		Revision as of 09:04, 18 April 2015
Line 53:		Line 53:
	/* Albert: Well, now I know, too! */		/* Albert: Well, now I know, too! */
	card({d\|Month\|->d : PD2 & KnowFromDay(PD2,d)})=1		card({d\|Month\|->d : PD2 & KnowFromDay(PD2,d)})=1

	ASSERTIONS /* single solution found by ProB in 20-30 ms */		ASSERTIONS /* single solution found by ProB in 20-30 ms */
	Month = "july";		Month = "july";

Michael Leuschel at 09:04, 18 April 2015

2015-04-18T09:04:22Z

← Older revision		Revision as of 09:04, 18 April 2015
Line 5:		Line 5:
	You can load this model using, e.g., ProB Tcl/Tk (see below). The model is also available as an example in our [[ProB_Logic_Calculator\|online ProB Logic Calculator]].		You can load this model using, e.g., ProB Tcl/Tk (see below). The model is also available as an example in our [[ProB_Logic_Calculator\|online ProB Logic Calculator]].

	In case you are new to B, you probably need to know the following operators to understand the specification below:		In case you are new to B, you probably need to know the following operators to understand the specification below (we als have a [[Summary_of_B_Syntax\|summary page about the B syntax]]):
	* <tt>x : S<tt> specifies that x is an element of S		* <tt>x : S<tt> specifies that x is an element of S
	* <tt>dom(r)</tt> is the domain of a function or relation		* <tt>dom(r)</tt> is the domain of a function or relation

Michael Leuschel at 08:43, 18 April 2015

2015-04-18T08:43:47Z

← Older revision		Revision as of 08:43, 18 April 2015
Line 5:		Line 5:
	You can load this model using, e.g., ProB Tcl/Tk (see below). The model is also available as an example in our [[ProB_Logic_Calculator\|online ProB Logic Calculator]].		You can load this model using, e.g., ProB Tcl/Tk (see below). The model is also available as an example in our [[ProB_Logic_Calculator\|online ProB Logic Calculator]].

	In case you are new to B, you probably need to know the following operators:		In case you are new to B, you probably need to know the following operators to understand the specification below:
	* <tt>x : S<tt> specifies that x is an element of S		* <tt>x : S<tt> specifies that x is an element of S
	* <tt>dom(r)</tt> is the domain of a function or relation		* <tt>dom(r)</tt> is the domain of a function or relation

Michael Leuschel at 08:43, 18 April 2015

2015-04-18T08:43:19Z

← Older revision		Revision as of 08:43, 18 April 2015
Line 6:		Line 6:

	In case you are new to B, you probably need to know the following operators:		In case you are new to B, you probably need to know the following operators:
	<tt>x : S<tt> specifies that x is an element of S		* <tt>x : S<tt> specifies that x is an element of S
	<tt>dom(r)</tt> is the domain of a function or relation		* <tt>dom(r)</tt> is the domain of a function or relation
	<tt>r~</tt> is the inverse of a function or relation		* <tt>r~</tt> is the inverse of a function or relation
	<tt>r[S]</tt> is the relational image of a relation r for a set of domain values S		* <tt>r[S]</tt> is the relational image of a relation r for a set of domain values S
	<tt>card(S)</tt> is the cardinality of a set		* <tt>card(S)</tt> is the cardinality of a set
	<tt>a\|->b</tt> represents the pair (a,b); note that a relation and function in B is a set of pairs.		* <tt>a\|->b</tt> represents the pair (a,b); note that a relation and function in B is a set of pairs.
			* <tt>!x.(P => Q)</tt> denotes universal quantification over variable x

	<pre>		<pre>

Michael Leuschel at 08:41, 18 April 2015

2015-04-18T08:41:58Z

← Older revision		Revision as of 08:41, 18 April 2015
Line 4:		Line 4:
	There are almost certainly more elegant encodings of the problem in B.		There are almost certainly more elegant encodings of the problem in B.
	You can load this model using, e.g., ProB Tcl/Tk (see below). The model is also available as an example in our [[ProB_Logic_Calculator\|online ProB Logic Calculator]].		You can load this model using, e.g., ProB Tcl/Tk (see below). The model is also available as an example in our [[ProB_Logic_Calculator\|online ProB Logic Calculator]].

			In case you are new to B, you probably need to know the following operators:
			<tt>x : S<tt> specifies that x is an element of S
			<tt>dom(r)</tt> is the domain of a function or relation
			<tt>r~</tt> is the inverse of a function or relation
			<tt>r[S]</tt> is the relational image of a relation r for a set of domain values S
			<tt>card(S)</tt> is the cardinality of a set
			<tt>a\|->b</tt> represents the pair (a,b); note that a relation and function in B is a set of pairs.

	<pre>		<pre>
Line 16:		Line 24:
	PROPERTIES		PROPERTIES
	/* Albert and Bernard just met Cheryl. “When’s your birthday?” Albert asked Cheryl.*/		/* Albert and Bernard just met Cheryl. “When’s your birthday?” Albert asked Cheryl.*/
	Month:STRING & Day:~~NATURAL1~~ &		Month:STRING & Day:1..31 &

	/* Cheryl thought a second and said, “I’m not going to tell you, but I’ll give you some clues.” She wrote down a list of 10 dates: */		/* Cheryl thought a second and said, “I’m not going to tell you, but I’ll give you some clues.” She wrote down a list of 10 dates: */

Michael Leuschel at 08:04, 16 April 2015

2015-04-16T08:04:36Z

← Older revision		Revision as of 08:04, 16 April 2015
Line 3:		Line 3:
	Here is a first solution in B, where the text of the puzzle has been integrated as comments.		Here is a first solution in B, where the text of the puzzle has been integrated as comments.
	There are almost certainly more elegant encodings of the problem in B.		There are almost certainly more elegant encodings of the problem in B.
	You can load this model using, e.g., ProB Tcl/Tk (see below). The model is also available as an example in our [[ProB_Logic_Calculator online ProB Logic Calculator]].		You can load this model using, e.g., ProB Tcl/Tk (see below). The model is also available as an example in our [[ProB_Logic_Calculator\|online ProB Logic Calculator]].

	<pre>		<pre>

Michael Leuschel at 08:04, 16 April 2015

2015-04-16T08:04:20Z

← Older revision		Revision as of 08:04, 16 April 2015
Line 3:		Line 3:
	Here is a first solution in B, where the text of the puzzle has been integrated as comments.		Here is a first solution in B, where the text of the puzzle has been integrated as comments.
	There are almost certainly more elegant encodings of the problem in B.		There are almost certainly more elegant encodings of the problem in B.
			You can load this model using, e.g., ProB Tcl/Tk (see below). The model is also available as an example in our [[ProB_Logic_Calculator online ProB Logic Calculator]].

	<pre>		<pre>