logic_programming/1_IntroProlog.ipynb

 %% Cell type:markdown id:7359298e-63ac-4080-9139-aa90c8043b2a tags:
 
 # Introduction to Prolog
 
 %% Cell type:markdown id:49fd5211 tags:
 
 ### Propositions
 Prolog programs consist of <b>clauses</b>.
 A clause is always terminated by a dot (```.```).
 The simplest clauses are facts. Here we define two propositions to be true:
 
 %% Cell type:code id:93e05f7b-a91c-4262-861e-a399e094b710 tags:
 
 ``` prolog
 rains.
 no_hat.
 ```
 
-%% Output
-
-
-
 %% Cell type:markdown id:b05ae74b tags:
 
 We can now ask the Prolog system whether it rains:
 
 %% Cell type:code id:20b05b2c tags:
 
 ``` prolog
 ?-rains.
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:50c188fa tags:
 
 More complicated clauses make use of the implication operator ```:-```. They are also called rules. Logically they stipulate that the left-hand side of the clause must be true if the right-hand side is true. The right-hand side can contain multiple propositions separated by commas. The comma can be read as a logical conjunction (and).
 
 %% Cell type:code id:2b8b84a0 tags:
 
 ``` prolog
 carry_umbrella :- rains, no_hat.
 ```
 
-%% Output
-
-
 %% Cell type:code id:4e6314e8 tags:
 
 ``` prolog
 ?- carry_umbrella.
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:161b0f75 tags:
 
 
 %% Cell type:markdown id:d7254b1b tags:
 
 ### Predicates
 Instead of propositions we can also use predicates with arguments within our clauses. The arguments to predicates denote objects for which the predicate is true. Arguments which start with an upper-case letter are logical variables. Below ```X``` is such a variable and it can stand for any object.
 
 %% Cell type:code id:1d6eed4f tags:
 
 ``` prolog
 human(sokrates).
 human(schopenhauer).
 human(locke).
 
 tiger(hobbes).
 
 mortal(X) :- human(X).
 mortal(X) :- animal(X).
 
 animal(X) :- tiger(X).
 ```
 
-%% Output
-
-
-
-
-
 %% Cell type:markdown id:e645f31e tags:
 
 You can now ask questions about logical consequences of your logic program. In simple queries you provide all arguments:
 
 %% Cell type:code id:a2ab9e95 tags:
 
 ``` prolog
 ?-human(locke).
 ```
 
 %% Output
 
 
 %% Cell type:code id:838bc91a tags:
 
 ``` prolog
 ?- human(hobbes).
 ```
 
 %% Output
 
 
 %% Cell type:code id:4d3217da tags:
 
 ``` prolog
 ?- animal(hobbes).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:c8d0600e tags:
 
 You can also use variables in queries, and Prolog will find values for the variables so that the result is a logical consequence of you program:
 
 %% Cell type:code id:93e47505 tags:
 
 ``` prolog
 ?- mortal(X).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:d82e2815 tags:
 
 In the standard Prolog console you can type a semicolong (```;```) to get more answers. Here in Jupyter we need to use ```jupyter:retry```.
 
 %% Cell type:code id:0c4d96e2 tags:
 
 ``` prolog
 jupyter:retry
 ```
 
 %% Output
 
 
-
 %% Cell type:code id:47e57f93 tags:
 
 ``` prolog
 jupyter:retry
 ```
 
 %% Output
 
 
-
 %% Cell type:code id:7fd70461 tags:
 
 ``` prolog
 jupyter:retry
 ```
 
 %% Output
 
 
-
 %% Cell type:code id:81724623 tags:
 
 ``` prolog
 jupyter:retry
 ```
 
 %% Output
 
 
-
 %% Cell type:markdown id:3dce4ccd tags:
 
 Jupyter provides a feature to compute all solutions of a goal and display them in a table:
 
 %% Cell type:code id:4d656338 tags:
 
 ``` prolog
 jupyter:print_table(mortal(X))
 ```
 
 %% Output
 
     X |
     :- |
     sokrates |
     schopenhauer |
     locke |
     hobbes |
 
 
 %% Cell type:markdown id:d90546b0 tags:
 
 Prolog also has a built-in predicate called ```findall``` which can be used to find all solutions in one go:
 
 %% Cell type:code id:a7478245 tags:
 
 ``` prolog
 ?-findall(X,mortal(X),Results).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:74c96ce2 tags:
 
 ### Prolog lists and using append
 The result is a Prolog list. Lists play an important role in Prolog and they can be written using square brackets. ```[]``` denotes the empty list. The built-in predicate ```append``` can be used to concatenate two lists:
 
 %% Cell type:code id:0352f53e tags:
 
 ``` prolog
 ?-append([sokrates,locke],[hobbes],R).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:fd8a78b7 tags:
 
 Lists can contain any kind of object, e.g., numbers but also other lists:
 
 %% Cell type:code id:9e3be61b tags:
 
 ``` prolog
 ?-append([1,2,sokrates,3],[4,[sokrates],4],Out).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:db2baf14 tags:
 
 One nice feature of logic programming is that the input/output relation is not pre-determined. One can run predicates backwards, meaning one can use ```append``` to deconstruct a list:
 
 %% Cell type:code id:186fe078 tags:
 
 ``` prolog
 ?-append(X,Y,[1,2,3]).
 ```
 
 %% Output
 
 
 %% Cell type:code id:de721f76 tags:
 
 ``` prolog
 jupyter:retry.
 ```
 
 %% Output
 
 
-
 %% Cell type:code id:ea9e3961 tags:
 
 ``` prolog
 jupyter:retry.
 ```
 
 %% Output
 
 
-
 %% Cell type:code id:e09505d2 tags:
 
 ``` prolog
 jupyter:retry.
 ```
 
 %% Output
 
 
-
 %% Cell type:code id:52857ccd tags:
 
 ``` prolog
 jupyter:retry.
 ```
 
 %% Output
 
 
-
 %% Cell type:markdown id:aacfbf9d tags:
 
 Variables can also appear multiple times in clauses or queries. Here we check if we can split a list in half:
 
 %% Cell type:code id:12f78859 tags:
 
 ``` prolog
 ?-append(X,X,[a,b,a,b]).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:16ffb236 tags:
 
 With the underscore we indicate that we are not interested in an argument; it is an anonymous logical variable. Here we use this to find the last element of a list:
 
 %% Cell type:code id:99bfae95 tags:
 
 ``` prolog
 ?-append(_,[X],[a,b,c,d]).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:466ece27 tags:
 
 ### Family tree example
 
 We now load a Prolog file describing the family tree of "Game of Thrones".
 
 %% Cell type:code id:5627c07e tags:
 
 ``` prolog
 :- consult('prolog_files/1_got_family_tree.pl').
 ```
 
 %% Cell type:markdown id:068e1fdc tags:
 
 It contains facts for four basic predicates male/1, female/1, child/2 and couple/2.
 
 %% Cell type:code id:428e3101 tags:
 
 ``` prolog
 ?-male(X).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:c2a8192b tags:
 
 We an now find the parents of X:
 
 %% Cell type:code id:5134897e tags:
 
 ``` prolog
 ?-male(X),child(X,Y).
 ```
 
 %% Output
 
 
 %% Cell type:code id:cd9a4bf2 tags:
 
 ``` prolog
 jupyter:retry.
 ```
 
 %% Output
 
 
-
 %% Cell type:markdown id:fa7eb5e5 tags:
 
 Let us now define derived predicates for father and mother:
 
 %% Cell type:code id:edfb9af1 tags:
 
 ``` prolog
 father(A,B) :- child(B,A),male(A).
 mother(A,B) :- child(B,A),female(A).
 ```
 
-%% Output
-
-
-
 %% Cell type:code id:e8aaec06 tags:
 
 ``` prolog
 ?-father(A,'Sansa Stark').
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:53b594a2 tags:
 
 We can visualise the father/mother relationships in graphical way in Jupyter:
 
 %% Cell type:code id:d4664fd8 tags:
 
 ``` prolog
 
 parent_relation(A,B,'father') :- father(A,B).
 parent_relation(A,B,'mother') :- mother(A,B).
 ```
 
-%% Output
-
-
-
 %% Cell type:code id:08715fa2 tags:
 
 ``` prolog
 jupyter:print_transition_graph(parent_relation/3, 1, 2, 3).
 ```
 
 %% Output
 
-
+
 
 
 %% Cell type:markdown id:e2ed5de7 tags:
 
 Let us now define the grandfather and grandmother relationships:
 
 %% Cell type:code id:313194bb tags:
 
 ``` prolog
 grandfather(A,B) :- child(B,C) , child(C,A), male(A).
 grandmother(A,B) :- child(B,C) , child(C,A), female(A).
 ```
 
-%% Output
-
-
-
 %% Cell type:code id:e0eed7cc tags:
 
 ``` prolog
 ?-grandfather(GF,'Sansa Stark').
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:d0e8eb01 tags:
 
 Finally let us use recursion in Prolog to define arbitrary ancestors:
 
 %% Cell type:code id:c2615402 tags:
 
 ``` prolog
 parent(A,B) :- child(B,A).
 ancestor(A,B):- parent(A,B).
 ancestor(A,B):- parent(C,B), ancestor(A,C).
 ```
 
-%% Output
-
-
-
-
 %% Cell type:code id:d2b8accc tags:
 
 ``` prolog
 ?-ancestor(GF,'Sansa Stark').
 ```
 
 %% Output
 
 
 %% Cell type:code id:05f68119 tags:
 
 ``` prolog
 jupyter:print_table(ancestor(X,'Sansa Stark'))
 ```
 
 %% Output
 
     X |
     :- |
     Eddard Stark |
     Catelyn Stark |
     Rickard Stark |
     Lyarra Stark |
 
 
 %% Cell type:markdown id:e6582326 tags:
 
 ### Send More Money Puzzle
 
 Prolog is also a natural language to solve constraint satisfaction problems. In particular the CLP(FD) library is very useful here. It allows to solve constraints over finite domains.
 
 %% Cell type:code id:da2e206f tags:
 
 ``` prolog
 :- use_module(library(clpfd)).
 ```
 
 %% Cell type:markdown id:8d8c47ed tags:
 
 The library provides a few operators like ```#=```, ```ins``` or ```all_different```:
 
 %% Cell type:code id:cf4ff4dd tags:
 
 ``` prolog
 ?- X #= Y+Z, [Y,Z] ins 0..9.
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:25e2db2a tags:
 
 To find solutions one needs to call ```labeling```:
 
 %% Cell type:code id:4f8aee37 tags:
 
 ``` prolog
 X #= Y+Z, [Y,Z] ins 0..9, labeling([],[Y,Z]).
 ```
 
 %% Output
 
 
 %% Cell type:code id:aac2c0ab tags:
 
 ``` prolog
 X #= Y+Z, [Y,Z] ins 0..9, all_different([X,Y,Z]), labeling([],[Y,Z]).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:ae23fbd6 tags:
 
 Let us now solve the Send More Money puzzle, where we have to find distinct digits such that this equation holds:
 ```
       S  E  N  D
 +     M  O  R  E
 =  M  O  N  E  Y
 ```
 
 %% Cell type:code id:c86fb33e tags:
 
 ``` prolog
 ?- L = [S,E,N,D,M,O,R,Y],
      L ins 0..9,  % all variables are digits
      S#>0, M#>0,  % S and M cannot be 1
      all_different(L), % all variables are different
                        1000*S + 100*E + 10*N + D
           +            1000*M + 100*O + 10*R + E
           #= 10000*M + 1000*O + 100*N + 10*E + Y,
      labeling([], L).
 ```
 
 %% Output
 
 
 %% Cell type:code id:deaef138 tags:
 
 ``` prolog
-juptyer:retry
+juptyer:retry.
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:5f251e4d tags:
 
+
+%% Cell type:markdown id:701bee1e tags:
+
+
+%% Cell type:markdown id:c600dcec tags:
+
+
+%% Cell type:markdown id:058bc4fb tags:
+

logic_programming/3_PropositionalLogic.ipynb

 %% Cell type:markdown id:9eb5530a tags:
 
 # Propositional Logic
 ## Syntax and Semantics Explained using a Prolog Implementation
 
 %% Cell type:markdown id:dba70591 tags:
 
 ## Well-Formed Formulas (WFF)
 
 All atomic propositions are WFF)
 If a und b are WFF then so are:
 - (¬ a)
 - (a ∧ b)
 - (a ∨ b)
 - (a → b)
 - (a ⟺ b)
 No other formulas are WFF.
 
 Note in the slides we use the single arrow `→` instead of the double arrow `⇒` for implication which is maybe more standard.
 
 Comment: a, b are metavariablens outside the syntax of propositional logic.
 
 %% Cell type:markdown id:dd01f86a tags:
 
 Maybe this reminds you of formal grammars from a theoretical computer science lecture.
 And indeed, the above can be written as a grammar using a non-terminal symbol wff.
 
 In Prolog, grammars can actually be written using DCG notation, which we will see and understand much later in the course.
 Here we simply write the grammar in Prolog style and can then use it to check if a formula is a WFF:
 
 %% Cell type:code id:964ebd52 tags:
 
 ``` prolog
  :- set_prolog_flag(double_quotes, codes).
 wff --> "p". % atomic proposition
 wff --> "q". % atomic proposition
 wff --> "(¬",wff,")".
 wff --> "(", wff, "∧", wff, ")".
 wff --> "(", wff, "∨", wff, ")".
 wff --> "(", wff, "→", wff, ")".
 wff --> "(", wff, "⟺", wff, ")".
+
+is_wff(String) :- wff(String,"").
+```
+
+%% Cell type:markdown id:87125415 tags:
+
+In Prolog string literals can be written using double quotes. Such literals are actually syntactic sugar for list of ASCII/Unicode numbers. (In most Prolog systems this is the default; in SWI Prolog you need to set the Prolog flag double_quotes to the value codes; see above).
+
+%% Cell type:code id:3d91dfdc tags:
+
+``` prolog
+?- X="p    q".
 ```
 
+%% Output
+
+
+%% Cell type:markdown id:15b8ea6b tags:
+
+We can use the above grammar and check whether a string is a well-formed formula:
+
 %% Cell type:code id:fc6823ad tags:
 
 ``` prolog
-?- wff("p","").
+?- is_wff("p").
+```
+
+%% Output
+
+
+%% Cell type:code id:a7168548 tags:
+
+``` prolog
+?- is_wff("p q").
 ```
 
 %% Output
 
 
 %% Cell type:code id:152289b6 tags:
 
 ``` prolog
-?- wff("(¬p)","").
+?- is_wff("(¬p)").
 ```
 
 %% Output
 
 
 %% Cell type:code id:2c3dd1bf tags:
 
 ``` prolog
-?- wff("(p∧(q∨(¬p)))","").
+?- is_wff("(p∧(q∨(¬p)))").
 %comment.
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:38b0a282 tags:
 
 This grammar does not talk about whitespace and requires parentheses for every connective used.
 In practice, one typically uses operator precedences to avoid having to write too many parentheses:
 - negation binds strongest
 - then come conjunction and disjunction
 - then come implication and equivalence.
 
 So instead of
 - (((¬ p) ∧ (¬ q)) → ((¬ p) ∨ (¬ q)))
 we can write
 - ¬ p ∧ ¬ q → ¬ p ∨ ¬ q
 
 We will try not not mix conjunction/disjunction and implication/equivalence without parentheses.
-We will also not try to improve our Prolog parser here to accomodate these precedences.
+We will also not improve our Prolog parser here to accomodate these precedences.
 This is the subject of another course (on compiler construction).
 
 %% Cell type:markdown id:92b6dc2d tags:
 
-We will also see much later that Prolog allows one to annotate grammars with semantic values, here to generate
+We now want to represent propositional logic formulas as Prolog terms. Simple propostions are translated into Prolog atoms, while for the logical connectives we use Prolog functors like not/1, and/2, ...:
+
+| Formula | Prolog Term |
+| --- | --- |
+| p | p |
+| (¬p) | not(p) |
+| (p ∧ q) | and(p,q) |
+| (p ∧ (¬p)) | and(p,not(p)) |
+
+We can actually generate those Prolog terms from the syntax of the formula using the following piece of Prolog code. Indeed, as we will see much later, Prolog allows one to annotate grammars with semantic values, here to generate
 a Prolog term representing the logical formal in the form of a syntax tree:
 
 %% Cell type:code id:78163b60 tags:
 
 ``` prolog
  :- set_prolog_flag(double_quotes, codes).
 wff(p) --> "p". % atomic proposition
 wff(q) --> "q". % atomic proposition
 wff(not(A)) --> "(¬",wff(A),")".
 wff(and(A,B)) --> "(", wff(A), "∧", wff(B), ")".
 wff(or(A,B)) --> "(", wff(A), "∨", wff(B), ")".
 wff(impl(A,B)) --> "(", wff(A), "→", wff(B), ")".
 wff(equiv(A,B)) --> "(", wff(A), "⟺", wff(B), ")".
 
 parse_wff(String,Formula) :- wff(Formula,String,"").
 ```
 
 %% Cell type:code id:6b9c3364 tags:
 
 ``` prolog
 ?- parse_wff("(¬p)",Formula).
 ```
 
 %% Output
 
 
 %% Cell type:code id:075dc3b2 tags:
 
 ``` prolog
 ?- parse_wff("(¬(p∧q))",Formula).
 ```
 
 %% Output
 
 
 %% Cell type:code id:338cb7dd tags:
 
 ``` prolog
-?- parse_wff("(p∧(q∨(¬p)))",Formula).
+?- parse_wff("(p∧(q∨(¬p)))",F).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:f9005519 tags:
 
 The above Prolog term `and(p,or(q,not(p)))` represents the logical formula in tree form.
 We can display the tree as a dag (directed acyclic graph) using the following subsidiary code
 (in future the Jupyter kernel will probably have a dedicated command to show a term graphically):
 
 %% Cell type:code id:f6116612 tags:
 
 ``` prolog
 subtree(Term,Nr,SubTerm) :-
    Term =.. [_|ArgList], %obtain arguments of the term
    nth1(Nr,ArgList,SubTerm). % get sub-argument and its position number
 
 % recursive and transitive closure of subtree
 rec_subtree(Term,Sub) :- Term = Sub.
 rec_subtree(Term,Sub) :- subtree(Term,_,X), rec_subtree(X,Sub).
 
 subnode(Sub,[shape/S, label/F],Formula) :-
    rec_subtree(Formula,Sub), % any sub-formula Sub of Formula is a node in the graphical rendering
    functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect).
+
 ```
 
 %% Cell type:code id:d7e68593 tags:
 
 ``` prolog
 jupyter:print_table(subnode(Node,Dot,and(p,or(q,not(p)))))
 ```
 
 %% Output
 
     Node | Dot |
     :- | :- |
     and(p,or(q,not(p))) | [shape/rect,label/and] |
     p | [shape/egg,label/p] |
     or(q,not(p)) | [shape/rect,label/or] |
     q | [shape/egg,label/q] |
     not(p) | [shape/rect,label/not] |
     p | [shape/egg,label/p] |
 
 
 %% Cell type:code id:3646e3ee tags:
 
 ``` prolog
+jupyter:show_graph(subnode(_,_,or(q,not(p))),subtree/3)
+```
+
+%% Output
+
+
+
+
+%% Cell type:code id:2aacffa9 tags:
+
+``` prolog
 jupyter:show_graph(subnode(_,_,and(p,or(q,not(p)))),subtree/3)
 ```
 
 %% Output
 
-
+
 
 
 %% Cell type:markdown id:11b3a8ad tags:
 
 Below we will study how one can assign a truth-value to logical formulas like the one above.
 
 ## Truth tables
 
 Every logical connective has a truth table, indicating how it maps the truth of its arguments to its own truth value.
-For example, `and` maps inputs `true` and `false` to `false`.
+For example, `and` maps inputs `true` and `false` to `false`. The truth table for the negation is:
+
+| a | not(a) |
+| --- | --- |
+| true | false |
+| false | true |
 
 Below we encode the truth table for five connectives as Prolog facts and rules.
 
 %% Cell type:code id:350b9756 tags:
 
 ``` prolog
 not(true,false).
 not(false,true).
 
 and(true,V,V) :- truth_value(V).
 and(false,V,false) :- truth_value(V).
 
 or(true,V,true) :- truth_value(V).
 or(false,V,V) :- truth_value(V).
 
 implies(A,B,Res) :- not(A,NotA), or(NotA,B,Res).
 equiv(A,B,Res) :- implies(A,B,AiB), implies(B,A,BiA), and(AiB,BiA,Res).
 
 truth_value(true).
 truth_value(false).
 
+% generate a single truth table for all connectives above:
 truth_table(A,B,NotA,AandB,AorB,AiB,AeB) :-
    truth_value(A), truth_value(B),
    not(A,NotA), and(A,B,AandB), or(A,B,AorB),
    implies(A,B,AiB), equiv(A,B,AeB).
 ```
 
 %% Cell type:markdown id:41cad0bc tags:
 
 We can now use the predicates `and/3`, ... to compute the truth value of the connectives for a particular input:
 
 %% Cell type:code id:3101448b tags:
 
 ``` prolog
-?- and(true,false,X).
+?- and(true,X,false).
 ```
 
 %% Output
 
 
 %% Cell type:code id:79d16b97 tags:
 
 ``` prolog
 ?- append([a],[b],R), append(R,[c],R2).
 ```
 
 %% Output
 
 
 %% Cell type:code id:d989abf2 tags:
 
 ``` prolog
 ?- and(X,true,true).
 ```
 
 %% Output
 
 
 %% Cell type:code id:922004e9 tags:
 
 ``` prolog
 ?- or(true,false,X).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:78c0eda3 tags:
 
 We can also display the whole truth table using a Jupyter command:
 
 %% Cell type:code id:54b57ff8 tags:
 
 ``` prolog
-jupyter:print_table(truth_table(A,B,NotA,AandB,AorB,AimpliesB,AequivB))
+jupyter:print_table(truth_table(A,B,Not_A,A_and_B,A_or_B,A_implies_B,A_equiv_B))
 ```
 
 %% Output
 
-    A | B | NotA | AandB | AorB | AimpliesB | AequivB |
+    A | B | Not_A | A_and_B | A_or_B | A_implies_B | A_equiv_B |
     :- | :- | :- | :- | :- | :- | :- |
     true | true | false | true | true | true | true |
     true | false | false | false | true | false | false |
     false | true | true | false | true | true | false |
     false | false | true | false | false | true | true |
 
 
 %% Cell type:markdown id:ce32b1d0 tags:
 
+### Interpretations ###
 An <b>interpretation</b> is an assignment of all relevant proposition to truth values (true or false).
 For example, given the formula `(p∧(q∨(¬p)))` an interpretation needs to assign a truth value to `p` and `q`.
 In the Prolog code below we will represent an interpretation as a list of bindings, each binding is a term of the form `Proposition/TruthValue`.
 For example, one of the four possible interpretations for the formula above is `[p/true, q/false]`.
 
 Using the built-in `member/2` predicate we can inspect an interpretation in Prolog. For example, here we retrieve the truth value of `q`:
 
+%% Cell type:code id:9a319a34 tags:
+
+``` prolog
+?- member(eq(z,X),[eq(p,1),eq(q,2),eq(z,222)]).
+```
+
+%% Output
+
+
+%% Cell type:code id:e425b0a3 tags:
+
+``` prolog
+?- member(/(z,X),[/(p,1),/(q,2),/(z,222)]).
+```
+
+%% Output
+
+
 %% Cell type:code id:8f6d804b tags:
 
 ``` prolog
 ?- Interpetation=[p/true, q/false],  member(p/P,Interpetation).
 ```
 
 %% Output
 
 
 %% Cell type:code id:da495155 tags:
 
 ``` prolog
 ?- Interpetation=[bind(p,true), bind(q,false)],  member(bind(q,Q),Interpetation).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:0d236e48 tags:
 
 Given an interpretation we can now compute the truth value for an entire formula in a recursive fashion.
 For propositions we look up the truth value in the interpretation (done using `member` below).
 For logical connectives we recursively compute the truth value of its arguments and then apply the truth tables we defined above.
 
 %% Cell type:code id:175c00d0 tags:
 
 ``` prolog
 value(X,Interpretation,Value) :-
    atomic(X), % we have a proposition
    member(X/Value,Interpretation).
 value(and(A,B),I,Val) :-
     value(A,I,VA), value(B,I,VB),
    and(VA,VB,Val).
 value(or(A,B),I,Val) :- value(A,I,VA), value(B,I,VB),
    or(VA,VB,Val).
 value(not(A),I,Val) :- value(A,I,VA),
    not(VA,Val).
 value(implies(A,B),I,Val) :- value(or(not(A),B),I,Val).
 value(equiv(A,B),I,Val) :-
    value(and(implies(A,B),implies(B,A)),I,Val).
 ```
 
 %% Cell type:markdown id:aa50ec0e tags:
 
 Using the above we can compute the truth value of `(p∧(q∨(¬p)))` for the interpretation `[p/true, q/false]`:
 
+%% Cell type:code id:ecd6951a tags:
+
+``` prolog
+?- value(not(p), [p/true, q/false],Res).
+```
+
+%% Output
+
+
 %% Cell type:code id:eee17774 tags:
 
 ``` prolog
 ?- value(and(p,or(q,not(p))), [p/true, q/false],Res).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:f3c2de52 tags:
 
 We can also use our parser instead of writing the logical formulas as Prolog terms:
 
 %% Cell type:code id:575fc20f tags:
 
 ``` prolog
 ?- parse_wff("(p∧(q∨(¬p)))",Formula), value(Formula, [p/true,q/false],Res).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:4387b4a2 tags:
 
+### Models ###
 The truth value of `(p∧(q∨(¬p)))` for the interpretation `[p/true, q/true]` is true.
 In this case the interpretation is called a <b>model</b> of the formula.
 
 %% Cell type:code id:fec75f65 tags:
 
 ``` prolog
 ?- value(and(p,or(q,not(p))), [p/true, q/true],Res).
 ```
 
 %% Output
 
 
+%% Cell type:code id:d88c023e tags:
+
+``` prolog
+?- value(and(p,or(q,not(p))), [p/P, q/Q],true).
+```
+
+%% Output
+
+
 %% Cell type:markdown id:3aa46665 tags:
 
 We can also compute the truth table of the entire formula, by trying out all possible interpretations.
 Below we leave P and Q as Prolog variable which is instantiated by the code above:
 
 %% Cell type:code id:78473da0 tags:
 
 ``` prolog
 jupyter:print_table(value(and(p,or(q,not(p))), [p/P, q/Q],Res))
 ```
 
 %% Output
 
     P | Q | Res |
     :- | :- | :- |
     true | true | true |
     true | false | false |
     false | true | false |
     false | false | false |
 
 
 %% Cell type:markdown id:5b4ee42b tags:
 
 Below we visualise graphically this computation, by displaying the syntax tree of a logical formula
 as a dag and by colouring the nodes using the `value` predicate:
 
 %% Cell type:code id:2ee60c15 tags:
 
 ``` prolog
 
 subnode_val(Sub,[shape/S, label/F, style/filled, fillcolor/C],Formula,Interpretation) :-
    rec_subtree(Formula,Sub), % any sub-formula Sub of Formula is a node in the graphical rendering
    get_label(Sub,F), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect),
    (value(Sub,Interpretation,true) -> C=olive ; C=sienna1).
 
 get_label(and(_,_),'∧') :- !.
 get_label(or(_,_),'∨') :- !.
 get_label(impl(_,_),'→') :- !.
 get_label(equiv(_,_),'⟺') :- !.
 get_label(not(_),'¬') :- !.
 get_label(Sub,F) :- functor(Sub,F,_).
 ```
 
 %% Cell type:code id:2b497dad tags:
 
 ``` prolog
 jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/false]),subtree/3)
 ```
 
 %% Output
 
-
+
 
 
 %% Cell type:code id:0fd23f05 tags:
 
 ``` prolog
 jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/true]),subtree/3)
 ```
 
 %% Output
 
-
+
 
 
 %% Cell type:markdown id:013fda69 tags:
 
+### Kinds of Formulas ###
 A formula for which all interpretations are models is called a <b>tautology</b>:
 
 %% Cell type:code id:23775624 tags:
 
 ``` prolog
 jupyter:print_table(value(or(p,not(p)), [p/P],Res))
 ```
 
 %% Output
 
     P | Res |
     :- | :- |
     true | true |
     false | true |
 
 
 %% Cell type:code id:7a6e29ed tags:
 
 ``` prolog
 jupyter:print_table(value(or(p,or(q,not(q))), [p/P, q/Q],Res))
 ```
 
 %% Output
 
     P | Q | Res |
     :- | :- | :- |
     true | true | true |
     false | true | true |
     true | false | true |
     false | false | true |
 
 
 %% Cell type:markdown id:9ff1936a tags:
 
 A formula which has no models is called a <b>contradiction</b>:
 
 %% Cell type:code id:6bd292f4 tags:
 
 ``` prolog
 jupyter:print_table(value(and(p,not(p)), [p/P],Res))
 ```
 
 %% Output
 
     P | Res |
     :- | :- |
     true | false |
     false | false |
 
 
 %% Cell type:markdown id:fc920c04 tags:
 
 A formula which has at least one model is called <b>satisfiable</b>.
 
 We can use our code above to find models, by leaving the interpretation of propositions as Prolog variables
 and by requiring the result to be `true`:
 
 %% Cell type:code id:ab15628a tags:
 
 ``` prolog
 ?-value(and(p,or(q,not(p))), [p/P, q/Q],true).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:64baad25 tags:
 
 The above is not a very efficient way of finding models.
 We return to this issue later.
 A tool that determines whehter a propositional logic formula is satisfiable and computes possibles models is called a <b>SAT solver</b>.
 
 %% Cell type:markdown id:8b2acc10 tags:
 
-
+### Logical Equivalence ###
 Two formulas are called <b>equivalent</b> iff they have the same models.
 We write this as `A ≡ B`.
 
 Below we can see that the models of `¬p ∨ q` and `p → q` are identical,
 i.e., `¬p ∨ q ≡ p → q`.
 
 %% Cell type:code id:68a2a19c tags:
 
 ``` prolog
 jupyter:print_table((user:value(or(not(p),q), [p/P, q/Q],NotPorQ),user:value(implies(p,q), [p/P, q/Q],PimpliesQ)))
 ```
 
 %% Output
 
     P | Q | NotPorQ | PimpliesQ |
     :- | :- | :- | :- |
     true | true | true | true |
     true | false | false | false |
     false | true | true | true |
     false | false | true | true |
 
 
 %% Cell type:code id:41f43345 tags:
 
 ``` prolog
 jupyter:print_table((user:value(and(p,q), [p/P, q/Q],PQ),user:value(and(q,p), [p/P, q/Q],QP)))
 ```
 
 %% Output
 
     P | Q | PQ | QP |
     :- | :- | :- | :- |
     true | true | true | true |
     true | false | false | false |
     false | true | false | false |
     false | false | false | false |
 
 
 %% Cell type:markdown id:248d3d32 tags:
 
+### Logical Consequence ###
 A formula `B` is the logical consequence of `A` if all models of `A` are also models of `B`.
 We write this as `A ⊨ B`.
 
 Below we can see that all models of `p ∧ q` are also models of `p ∨ q`,
 i.e., `p ∧ q ⊨ p ∨ q`.
 
 %% Cell type:code id:aaf46953 tags:
 
 ``` prolog
 jupyter:print_table((user:value(and(p,q), [p/P, q/Q],PandQ),user:value(or(p,q), [p/P, q/Q],PorQ)))
 ```
 
 %% Output
 
     P | Q | PandQ | PorQ |
     :- | :- | :- | :- |
     true | true | true | true |
     true | false | false | true |
     false | true | false | true |
     false | false | false | false |
 
 
 %% Cell type:markdown id:3e261892 tags:
 
 ## Improving our Prolog program
 
 For convenience we now write some piece of Prolog code to find the atomic propositions used within a formula.
 This obviates the need to write interpretation skeletons like `[p/P,q/Q]` ourselves.
 
 %% Cell type:code id:da0a82b5 tags:
 
 ``` prolog
 get_aps(Formula,SortedPropositions) :-
     findall(P, ap(Formula,P), Ps), sort(Ps,SortedPropositions).
-% extract atomic propostions used by formula
+% extract atomic propostions used by formula as a list
 ap(X,X) :- atomic(X).
 ap(and(A,B),AP) :- ap(A,AP) ; ap(B,AP).
 ap(or(A,B),AP) :- ap(A,AP) ; ap(B,AP).
 ap(implies(A,B),AP) :- ap(A,AP) ; ap(B,AP).
 ap(equiv(A,B),AP) :- ap(A,AP) ; ap(B,AP).
 ap(not(A),AP) :- ap(A,AP).
 ```
 
 %% Cell type:code id:a216799f tags:
 
 ``` prolog
 ?- ap(and(p,q),AP).
 ```
 
 %% Output
 
 
 %% Cell type:code id:8a38f7cc tags:
 
 ``` prolog
 jupyter:retry
 ```
 
 %% Output
 
 
 %% Cell type:code id:82980216 tags:
 
 ``` prolog
 ?- get_aps(and(p,q),Ps).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:e4c2468b tags:
 
 We can now write a more convenient predicate to find models for a formula:
 
 %% Cell type:code id:23cfb806 tags:
 
 ``` prolog
 sat(Formula,Interpretation) :-
    get_aps(Formula,SPs),
    skel(SPs,Interpretation), % set up interpretation skeleton
    value(Formula,Interpretation,true).
 
 skel([],[]).
 skel([AP|T],[AP/_|ST]) :- skel(T,ST). % we replace p by p/_ so that we have an unbound logical varible for every proposition
 
 unsat(Formula) :- \+ sat(Formula,_). % a formula is unsatisfiable if we can find no model, \+ is Prolog negation
 ```
 
 %% Cell type:markdown id:c98b7052 tags:
 
 The skel predicate simply takes a list of propositions and generates a skeleton interpretation with fresh logical variables for the truth values:
 
 %% Cell type:code id:da991b8d tags:
 
 ``` prolog
 ?- skel([a,b,c],R).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:9444e54a tags:
 
 We can now use `sat/2` to compute models, without having to provide ourselves an interpretation skeleton:
 
 %% Cell type:code id:6338f6bf tags:
 
 ``` prolog
 ?- sat(and(p,or(q,not(p))),Model).
 ```
 
 %% Output
 
 
 %% Cell type:code id:266a4bd8 tags:
 
 ``` prolog
 ?- unsat(and(p,not(p))).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:9fb0715e tags:
 
 ## Proof by contradiction
 
 To prove that `B` is a logical consequence of `A` we can employ a <b>proof by contradiction</b>:
 - assume that `B` is false and
 - show that this leads to a contradiction.
 
 %% Cell type:code id:6957d9f3 tags:
 
 ``` prolog
 prove(A,B) :- /* prove that B follows from A */
    unsat(and(A,not(B))).
 
 equivalent(A,B) :- prove(A,B), prove(B,A).
 ```
 
+%% Cell type:markdown id:0164a7ec tags:
+
+For example, we can now prove that ```p or q``` is a logical consequence of ```p and q```:
+
 %% Cell type:code id:f552a71e tags:
 
 ``` prolog
 ?- prove(and(p,q),or(p,q)).
 ```
 
 %% Output
 
 
+%% Cell type:markdown id:0f4331e3 tags:
+
+However, the logical consequence does not hold the other way around:
+
 %% Cell type:code id:76b8ab5a tags:
 
 ``` prolog
 ?- prove(or(p,q),and(p,q)).
 ```
 
 %% Output
 
 
 %% Cell type:code id:f8aca8b7 tags:
 
 ``` prolog
 ?- equivalent(and(p,q),or(p,q)).
 ```
 
 %% Output
 
 
+%% Cell type:markdown id:e60f533e tags:
+
+As usual in classical logic, anything is a consequence of a contradiction:
+
 %% Cell type:code id:e7a2828d tags:
 
 ``` prolog
+?- prove(and(p,not(p)),q).
+```
+
+%% Output
+
+
+%% Cell type:code id:47dd7088 tags:
+
+``` prolog
 ?- prove(and(p,not(p)),and(q,not(q))).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:02395cde tags:
 
 In case something is not a logical consequence we can use this code to find an explanation (aka counter example):
 
 %% Cell type:code id:26bab55b tags:
 
 ``` prolog
 disprove(A,B,CounterExample) :- /* show why B does not follow from A */
    sat(and(A,not(B)),CounterExample).
 ```
 
 %% Cell type:code id:fe5daeb4 tags:
 
 ``` prolog
 ?- disprove(or(p,q),and(p,q),Counter).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:870939fa tags:
 
 ## Some Puzzles
 
 We can return to our Knights & Knave puzzle from the first lecture.
 There is an island populated by only knights and knaves.
 Knights always say the truth and knaves always lie.
 We encounter three persons A,B,C on this island:
 - 1. A says: “B is a knave oder C is a knave”
 - 2. B says: “A is a knight”
 
 %% Cell type:code id:3187bee7 tags:
 
 ``` prolog
 ?- sat(and(equiv(a,or(not(b),not(c))),equiv(b,a)),I).
 ```
 
 %% Output
 
 
+%% Cell type:markdown id:31253833 tags:
+
+And we can find no further solution to this query:
+
+%% Cell type:code id:b79ef066 tags:
+
+``` prolog
+jupyter:retry.
+```
+
+%% Output
+
+
 %% Cell type:markdown id:575d68a0 tags:
 
-We can also prove that this is the only solution, i.e., our puzzle implies that A and B are knights and C is a knave:
+We can also prove explicitly that this is the only solution, i.e., our puzzle implies that A and B are knights and C is a knave:
 
 %% Cell type:code id:df153b0a tags:
 
 ``` prolog
 ?- prove(and(equiv(a,or(not(b),not(c))),equiv(b,a)), and(a,and(b,not(c)))).
 ```
 
 %% Output
 
 
 %% Cell type:code id:1712e9e0 tags:
 
 ``` prolog
 jupyter:show_graph(subnode_val(_,_,and(equiv(a,or(not(b),not(c))),equiv(b,a)),[a/true,b/true,c/false]),subtree/3).
 ```
 
 %% Output
 
-
+
 
 
 %% Cell type:markdown id:c0299ea9 tags:
 
 Let us now model another puzzle from Raymond Smullyan.
 
 - The King says: One note tells the truth and one does not
 - Note on Door 1: This cell contains a princess and there is a tiger in the other cell
 - Note on Door 2: One of the cells contains a princess and the other one contains a tiger.
 
+The propositions are
+- z1: note on door 1 is true
+- z2: note on door 2 is true
+- t1: there is a tiger behind door 1 (and no princess behind door 1)
+- t2: there is a tiger behind door 2 (and no princess behind dorr 2)
+We assume that if t1 is false, then there is a princess behind the door. The same holds for t2.
 
 %% Cell type:code id:4363c114 tags:
 
 ``` prolog
-?- sat(and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))),I).
+?- sat(and(equiv(z1,not(z2)),
+       and(equiv(z1,and(not(t1),t2)),
+           equiv(z2,equiv(t1,not(t2))))),I).
 ```
 
 %% Output
 
 
 %% Cell type:code id:0919b40c tags:
 
 ``` prolog
 jupyter:retry.
 ```
 
 %% Output
 
 
+%% Cell type:markdown id:38574a7c tags:
+
+Below is an encoding of the puzzle where we do not assume that each cell has either a tiger or a princess; hence we have two atomic propositions per cell (t1,p1 and t2,p2). In this case we do not have a unique solution. So the knowledge that each cell contains one tiger or princess is essential.
+
+%% Cell type:code id:f2b747ca tags:
+
+``` prolog
+?- sat(and(equiv(z1,not(z2)),
+       and(equiv(z1,and(p1,t2)),
+           equiv(z2,or(and(p1,t2),and(p2,t1))))),I).
+```
+
+%% Output
+
+
+%% Cell type:code id:d734608a tags:
+
+``` prolog
+jupyter:retry.
+```
+
+%% Output
+
+
+%% Cell type:markdown id:1eaff825 tags:
+
+If we add explicitly that t1 is equivalent to not(p1) and ditto for t2 then we have a single solution:
+
+%% Cell type:code id:39802240 tags:
+
+``` prolog
+?- sat(and(equiv(z1,not(z2)),
+       and(equiv(t1,not(p1)),
+       and(equiv(t2,not(p2)),
+       and(equiv(z1,and(p1,t2)),
+           equiv(z2,or(and(p1,t2),and(p2,t1))))))),I).
+```
+
+%% Output
+
+
+%% Cell type:code id:becfaa25 tags:
+
+``` prolog
+jupyter:retry.
+```
+
+%% Output
+
+
 %% Cell type:code id:f64a00fe tags:
 
 ``` prolog
 jupyter:show_graph(subnode_val(_,_,and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))),
                               [t1/true,t2/false,z1/false,z2/true]),subtree/3).
 ```
 
 %% Output
 
-
+
 
 
 %% Cell type:markdown id:35fba4c7 tags:
 
 ### Appendix: Generating equivalent formulas
 
 %% Cell type:markdown id:78beaf88 tags:
 
 The code below can be used to generate formulas in Prolog using a technique similar to iterative deepening.
 We will study this technique much later in the course in the lectures on search.
 All you need to know is that generate_formula generates formulas from smaller to deeper formulas.
 
 %% Cell type:code id:51d5630b tags:
 
 ``` prolog
 generate_formula(X) :-
    peano(MaxDepth), gen(X,MaxDepth).
 peano(0).
 peano(s(X)) :- peano(X).
 
 proposition(p).
 proposition(q).
 proposition(r).
 
 gen(X,_) :- proposition(X).
 gen(and(A,B),s(MaxDepth)) :- gen(A,MaxDepth), gen(B,MaxDepth).
 gen(or(A,B),s(MaxDepth)) :- gen(A,MaxDepth), gen(B,MaxDepth).
 gen(implies(A,B),s(MaxDepth)) :- gen(A,MaxDepth), gen(B,MaxDepth).
 gen(equiv(A,B),s(MaxDepth)) :- gen(A,MaxDepth), gen(B,MaxDepth).
 gen(not(A),s(MaxDepth)) :- gen(A,MaxDepth).
 ```
 
 %% Cell type:code id:f843534d tags:
 
 ``` prolog
 ?-generate_formula(X).
 ```
 
 %% Output
 
 
 %% Cell type:code id:3e0e951d tags:
 
 ``` prolog
 jupyter:retry.
 ```
 
 %% Output
 
 
 %% Cell type:code id:8199e19a tags:
 
 ``` prolog
 jupyter:retry.
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:cd56c6d2 tags:
 
 We can now use this together with our other Prolog predicates to generate equivalent formulas:
 
 %% Cell type:code id:fae03e15 tags:
 
 ``` prolog
 ?- generate_formula(Formula), equivalent(and(p,q),Formula), Formula \= and(p,q).
 ```
 
 %% Output
 
 
 %% Cell type:code id:94b16168 tags:
 
 ``` prolog
 jupyter:retry.
 ```
 
 %% Output
 
 
 %% Cell type:code id:a49ecd78 tags:
 
 ``` prolog
 ?- generate_formula(Formula), equivalent(and(p,p),Formula).
 ```
 
 %% Output
 
 
 %% Cell type:code id:49caff90 tags:
 
 ``` prolog
 ?- generate_formula(Formula), equivalent(and(p,or(p,q)),Formula).
 ```
 
 %% Output
 
 
 %% Cell type:markdown id:c57cbe05 tags:
 
 Another side note: we can use the $Var feature of Jupyter Prolog to combine the parser and the show_graph feature:
 
 %% Cell type:code id:c1766e98 tags:
 
 ``` prolog
 ?- parse_wff("(p∧(q∨(¬p)))",Formula).
 ```
 
 %% Output
 
 
 %% Cell type:code id:0fd61d87 tags:
 
 ``` prolog
 jupyter:show_graph(subnode_val(_,_,$Formula,[p/true,q/true]),subtree/3).
 ```
 
 %% Output
 
-
+
 
 
 %% Cell type:code id:78693e86 tags:
 
 ``` prolog
 ```
 
 %% Cell type:code id:5e50f3c7 tags:
 
 ``` prolog
 ```

sks/1_B_Sprache.ipynb

 %% Cell type:markdown id: tags:
 
 # Vorlesung: B Sprache
 
 %% Cell type:markdown id: tags:
 
 ## Struktur von Event-B Modellen
 
 Ein Event-B System besteht aus
 * statischen Teilen: die Kontexte
 - definieren Konstanten, Basismengen, Axiome, Theoreme
 * dynamischen Teilen: Maschinen
 - definieren Variablen, Ereignisse, Invarianten
 
 * Kontexte können von Maschinen gesehen werden
 * Kontexte und Maschinen können verfeinert werden
 
 %% Cell type:markdown id: tags:
 
 ## Syntaktische Klassen
 Es gibt drei Arten von Formeln in B:
 - **Ausdrücke** (Expressions): haben einen Wert, verändern den Zustand einer B Maschine *nicht*
 - **Prädikate** (Predicates): sind wahr oder falsch, haben *keinen* Wert und verändern den Zustand der Maschine *nicht*
 - **Anweisungen** (Substitutions, Statements): haben keinen Wert, können aber den Zustand einer Maschine verändern
 
 Anweisungen sind zB `x := x+1` und können nur in Maschinen, nicht in Kontexten verwendet werden.
 
 %% Cell type:markdown id: tags:
 
 Dies ist ein Ausdruck in B:
 
 %% Cell type:code id: tags:
 
 ``` prob
 2+3
 ```
 
 %% Output
 
     $5$
     5
 
 %% Cell type:markdown id: tags:
 
 Dies ist ein Prädikat in B:
 
 %% Cell type:code id: tags:
 
 ``` prob
 2>3
 ```
 
 %% Output
 
     $\mathit{FALSE}$
     FALSE
 
 %% Cell type:markdown id: tags:
 
 B unterscheidet streng zwischen den Bool'schen Werten TRUE und FALSE und zwischen Prädikaten die wahr und falsch sind. Folgendes ist ein valider Ausdruck in B und beschreibt die Menge bestehend aus dem Bool'schen Wert `FALSE`:
 
 %% Cell type:code id: tags:
 
 ``` prob
 {FALSE}
 ```
 
 %% Output
 
     $\{\mathit{FALSE}\}$
     {FALSE}
 
 %% Cell type:markdown id: tags:
 
 Folgendes ist **kein** valider Ausdruck in B:
 
 %% Cell type:code id: tags:
 
 ``` prob
 {bool(2>3)}
 ```
 
 %% Output
 
     $\{\mathit{FALSE}\}$
     {FALSE}
 
 %% Cell type:markdown id: tags:
 
 ## Syntax
 
 Die meisten Operatoren in B können entweder als ASCII Zeichenkette oder als Unicode Symbol eingegeben werden.
 Hier verwenden wir zum Beispiel die Unicode Version von ```/``` für die Division:
 
 %% Cell type:code id: tags:
 
 ``` prob
 10 ÷ 2
 ```
 
 %% Output
 
     $5$
     5
 
 %% Cell type:markdown id: tags:
 
 
 Die Syntax von Event-B und klassischem B unterscheidet sich leicht.
 In Rodin muss man Event-B Syntax verwenden; Jupyter verwendet standardmäßig klassisches B.
 
 Zum Beispiel benutzt Rodin `^` zum Potenzieren, während man im klassische B `**` verwendet:
 
 %% Cell type:code id: tags:
 
 ``` prob
 2**100
 ```
 
 %% Output
 
     Error from ProB: ERROR
     2 errors:
     Error: Type mismatch: Expected POW(_A), but was INTEGER in '2'
     Error: Type mismatch: Expected POW(_A), but was INTEGER in '100'
 
 %% Cell type:markdown id: tags:
 
 In Rodin wird `**` für das kartesische Produkt verwendet, im klassischen B verwendet man dafür `*`.
 Wir laden jetzt ein leeres Event-B Modell um den Parser in den Event-B Modus zu wechseln.
 Man kann auch das Kommando ```:language event_b``` verwenden um den Parser umzustellen.
 Mit ```:language classical_b``` kann man zurück zum normalen B Parser wechseln.
 Wenn man eine B Maschine oder einen Kontext lädt wechselt der Parser in den richtigen Modus.
 Hier laden wir einen leeren Event-B Kontext; dadurch wechselt der Parser in den Event-B Modus:
 
 %% Cell type:code id: tags:
 
 ``` prob
 :load models/empty_ctx.eventb
 ```
 
 %% Output
 
     Loaded machine: empty_ctx
 
 %% Cell type:code id: tags:
 
 ``` prob
 2^100
 ```
 
 %% Output
 
     $1267650600228229401496703205376$
     1267650600228229401496703205376
 
 %% Cell type:markdown id: tags:
 
 ## Semantische Grundlage von B
 
 * Arithmetik (ganze Zahlen)  ÷   +   −   ≤
 * Prädikatenlogik  ⇒   ∀
 * Mengentheorie  ∩   ∪   ⊆   ∈
 * Paare
 * Relationen,Funktionen, Sequenzen/Folgen, Bäume
 
 %% Cell type:markdown id: tags:
 
 ## Aussagenlogik
 
 B unterstützt folgende Junktoren der Aussagenlogik:
 
 Junktor | ASCII | Unicode
 -------|-------|-----
 Konjunktion | & | ∧
 Disjunktion | or | ∨
 Negation | not | ¬
 Implikation | => | ⇒
 Äquivalenz | <=> | ⇔
 
 Mit `:prettyprint` kann man sich die Unicode Version einer Formel ausgeben lassen:
 
 %% Cell type:code id: tags:
 
 ``` prob
 :prettyprint not(2>3 or 4>2) <=> 5>2
 ```
 
 %% Output
 
     $\neg (2 > 3 \vee  4 > 2) \mathbin\Leftrightarrow  5 > 2$
     ¬(2 > 3 ∨ 4 > 2) ⇔ 5 > 2
 
 %% Cell type:markdown id: tags:
 
 Man kann eine Aussage natürlich auch auswerten:
 
 %% Cell type:code id: tags:
 
 ``` prob
 not(2>3 or 4>2) ⇔ 5>2
 ```
 
 %% Output
 
     $\mathit{FALSE}$
     FALSE
 
 %% Cell type:code id: tags:
 
 ``` prob
 2>3 or 4>2
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 not(2>3 or 4>2)
 ```
 
 %% Output
 
     $\mathit{FALSE}$
     FALSE
 
 %% Cell type:code id: tags:
 
 ``` prob
 5>2
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:markdown id: tags:
 
 ### Prioritäten
 
 * höchste Priorität: ¬
 * danach ∧ , ∨
 * danach ⇒ , ⇔
 
 %% Cell type:code id: tags:
 
 ``` prob
 2>0 or 3>4 ⇒ 4>5
 ```
 
 %% Output
 
     $\mathit{FALSE}$
     FALSE
 
 %% Cell type:code id: tags:
 
 ``` prob
 2>0 or (3>4 ⇒ 4>5)
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 (2>0 or 3>4) ⇒ 4>5
 ```
 
 %% Output
 
     $\mathit{FALSE}$
     FALSE
 
 %% Cell type:code id: tags:
 
 ``` prob
 (1=1 => 2=2) => 3=1
 ```
 
 %% Output
 
     $\mathit{FALSE}$
     FALSE
 
 %% Cell type:markdown id: tags:
 
 *Achtung:*
 * in Rodin/Event-B haben Konjunktion und Disjunktion die gleiche Priorität und dürfen nicht ohne Klammerung gemischt werden. In klassischem B schon.
 * Das gleiche gilt für => und <=>.
 * In Rodin ist auch keine Assoziativität für => oder <=> definiert worden. Man darf diese Operatoren also auch nicht untereinander ohne Klammern mischen.
 
 %% Cell type:code id: tags:
 
 ``` prob
 2>1 or 2>3 & 3>4
 ```
 
 %% Output
 
     de.prob.animator.domainobjects.EvaluationException: Could not parse formula:
     Parsing predicate failed because: Operator: ∨ is not compatible with: ∧, parentheses are required
 
     Operator: ∨ is not compatible with: ∧, parentheses are required
     Parsing expression failed because: Operator: ∨ is not compatible with: ∧, parentheses are required
 
     Operator: ∨ is not compatible with: ∧, parentheses are required
     Parsing substitution failed because: Unknown operator:  (expected to find an assignment operator)
 
     Unknown operator:  (expected to find an assignment operator)
     Code: 2>1 or 2>3 & 3>4
     Unicode translation: 2>1 ∨ 2>3 ∧ 3>4
 
 %% Cell type:markdown id: tags:
 
 ## Prädikate
 
 In Event-B gibt es die Aussagen true (⊤) und false (⊥)  (nicht verwechseln mit den Bool'schen Datenwerten TRUE und FALSE). Im klassichen B gibt es diese beiden Aussagen nicht (wobei ProB `btrue` und `bfalse` akzeptiert).
 
 
 %% Cell type:code id: tags:
 
 ``` prob
 true or false
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 ⊤ or ⊥
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:markdown id: tags:
 
 
 Wahrheitswerte können über Prädikate hergestellt werden:
 * ein n-äres Pradikat bekommt n Datenwerte und bildet diese auf einen Wahrheitswert ab
 
 Für alle Datentypen gibt es die binären Pradikate = und ≠ (wobei gilt x ≠ y ⇔ ¬(x=y)).
 Für Zahlen gibt es die mathematischen Vergleichsoperatoren. Für Mengen werden noch weitere Prädikate hinzukommen.
 
 %% Cell type:code id: tags:
 
 ``` prob
 2 = 3-1
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 3 ≠ 3+1
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 4 >= 2+2
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:markdown id: tags:
 
 ## Quantoren
 
 In B gibt es zwei Quantoren die neue Variablen einführen:
 * den Existenzquantor (mindestens eins)
  - #x.(P) als ASCII
  - ∃x.(P) als Unicode
 * den Allquantor/Universalquantor (alle / jeder)
  - !x.(P => Q) als ASCII
  - ∀(x).(P ⇒ Q) als Unicode
 
  Der Rumpf eines Allquantors muss also immer eine Implikation auf oberster Ebene verwenden.
 
 %% Cell type:code id: tags:
 
 ``` prob
 ∃x .(  x>2 )
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 ∀x .( x>2 ⇒ x>3 )
 ```
 
 %% Output
 
     $\mathit{FALSE}$
     
     **Solution:**
     * $\mathit{x} = 3$
     FALSE
     
     Solution:
     	x = 3
 
 %% Cell type:code id: tags:
 
 ``` prob
 ∀x .( x>2 & x < 100 ⇒  ∃y.(x=y+y))
 ```
 
 %% Output
 
     $\mathit{FALSE}$
     
     **Solution:**
     * $\mathit{x} = 3$
     FALSE
     
     Solution:
     	x = 3
 
 %% Cell type:code id: tags:
 
 ``` prob
 ∀x .( x>2 & x < 100 ⇒  ∃y.(x=y+y) or ∃y.(x=y+y+1))
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:markdown id: tags:
 
 ### Typisierung bei Quantoren
 
 B basiert auf typisierter Logik
 * Bei Quantoren, zum Beispiel, müssen die neuen Variablen typisiert werden
  - ∃x.(2>3)  ist nicht erlaubt
 
 Generell: für   ∃x.(P)  und  ∀(x).(P ⇒ Q)  muss P den Typen von x bestimmbar machen.
 Deshalb ist der Rumpf eines Allquantors auch immer eine Implikation.
  Beim Existenzquantor wird oft eine Konjunktion verwendet.
  Warum macht eine Implikation beim Existenzquantor fast nie Sinn?
 
 %% Cell type:code id: tags:
 
 ``` prob
 ∃x.(x>-100000 => 22=1)
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:markdown id: tags:
 
 ## Arithmetik
 
 B bietet Arithmetik über *ganzen* Zahlen an.
 
 Folgende Zahlenmengen sind vordefiniert:
 * INT, ℤ
 * NAT = {x|x≥0}, ℕ
 * NAT1= {x|x≥1}, ℕ1
 
 In Atelier-B (klassisches B für die Softwareentwicklung, nicht in Rodin) wird zwischen mathematischen und implementierbaren Zahlen unterschieden:
 * Mathematische ganze Zahlen: INTEGER, NATURAL, NATURAL1
 * Implementierbare ganze Zahlen: INT, NAT, NAT1
 * MININT, MAXINT
 
 NATURAL aus dem klassischem B entspricht also NAT in Rodin.
 NAT aus dem klassischen B entspricht 0..MAXINT in Rodin, wobei MAXINT als Konstante definiert werden muss.
 
 %% Cell type:code id: tags:
 
 ``` prob
 0:ℕ
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 0:NAT1
 ```
 
 %% Output
 
     $\mathit{FALSE}$
     FALSE
 
 %% Cell type:markdown id: tags:
 
 ### Divsion
 
 B benutzt ganzzahlige Division und es gilt zB das Gesetz
 *  b≠0 ⇒ a ÷ b = (−a) ÷ (−b)
 Man hat auch:
 
 %% Cell type:code id: tags:
 
 ``` prob
 3/2
 ```
 
 %% Output
 
     $1$
     1
 
 %% Cell type:code id: tags:
 
 ``` prob
 -3 / 2
 ```
 
 %% Output
 
     $-1$
     −1
 
 %% Cell type:markdown id: tags:
 
 In Python bekommt man
 ```
 >>> (-3)//2
 -2
 ```
 
 %% Cell type:markdown id: tags:
 
 Division durch 0 und modulo durch negative Zahlen ist nicht definiert.
 
 %% Cell type:code id: tags:
 
 ``` prob
 100 mod -2
 ```
 
 %% Output
 
     :eval: NOT-WELL-DEFINED:
     mod not defined for negative numbers: 100 mod-2
 
 %% Cell type:markdown id: tags:
 
 ## Mengen
 
 Mengen sind ein fundamentales Konzept in B.
 In eine Mengen darf man nur Werten eines gleichen Typs packen.
 Mengen dürfen aber verschachtelt werden.
 
 Die einfachste Menge ist die leere Menge:
 
 %% Cell type:code id: tags:
 
 ``` prob
 {}
 ```
 
 %% Output
 
     $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
     ∅
 
 %% Cell type:markdown id: tags:
 
 Man kann Mengen durch **explizite Aufzählung** (Enumeration, set extension auf Englisch) definieren:
 
 %% Cell type:code id: tags:
 
 ``` prob
 {1,1+1,2,2+2,3,4}
 ```
 
 %% Output
 
     $\{1,2,3,4\}$
     {1,2,3,4}
 
 %% Cell type:markdown id: tags:
 
 Mengen können auch mit Hilfe eines Prädikats definiert werden (set comprehension auf Englisch). Die Syntaxform ist `{x | P}`.
 
 %% Cell type:code id: tags:
 
 ``` prob
 {x | x>0 & x<5}
 ```
 
 %% Output
 
     $\{1,2,3,4\}$
     {1,2,3,4}
 
 %% Cell type:code id: tags:
 
 ``` prob
 {x|x>2+2}
 ```
 
 %% Output
 
     $\{\mathit{x}\mid\mathit{x} > 4\}$
     {x∣x > 4}
 
 %% Cell type:markdown id: tags:
 
 Eine Menge an Zahlen kann auch mit der Intervallnotation ``a..b`` definiert werden:
 
 %% Cell type:code id: tags:
 
 ``` prob
 1..4
 ```
 
 %% Output
 
     $\{1,2,3,4\}$
     {1,2,3,4}
 
 %% Cell type:markdown id: tags:
 
 Die Kardinalität (Mächtigkeit) einer endlichen Menge kann mit dem card Operator bestimmt werden:
 
 %% Cell type:code id: tags:
 
 ``` prob
 card({1,1+1,2,2+2,3,4})
 ```
 
 %% Output
 
     $4$
     4
 
 %% Cell type:code id: tags:
 
 ``` prob
 card({x|x>2})
 ```
 
 %% Output
 
-    :eval: NOT-WELL-DEFINED:
-    card applied to very large set, cardinality not representable in ProB:  closure([x],[integer],b(greater(b(identifier(...),integer,[...]),b(value(...),integer,[...])),pred,[nodeid(none)]))
+    Error from ProB: NOT-WELL-DEFINED
+    Error: card applied to infinite set, cardinality not representable in ProB:  {x|x > 2} (:1:0 to 1:13)
+    card({x|x>2})
 
 %% Cell type:markdown id: tags:
 
 Mengen können andere Mengen beinhalten:
 
 %% Cell type:code id: tags:
 
 ``` prob
 { 1..4 , {1,2,3,4,2+2}, {}}
 ```
 
 %% Output
 
     $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1,2,3,4\}\}$
     {∅,{1,2,3,4}}
 
 %% Cell type:code id: tags:
 
 ``` prob
 card({ 1..4 , {1,2,3,4,2+2}, {}})
 ```
 
 %% Output
 
     $2$
     2
 
 %% Cell type:markdown id: tags:
 
 Was ist der Untschied zwischen der leeren Menge ∅ und { ∅ }?
 
 %% Cell type:code id: tags:
 
 ``` prob
 ∅ = {∅}
 ```
 
 %% Output
 
     $\mathit{FALSE}$
     FALSE
 
 %% Cell type:code id: tags:
 
 ``` prob
 card(∅)
 ```
 
 %% Output
 
     $0$
     0
 
 %% Cell type:code id: tags:
 
 ``` prob
 card({∅})
 ```
 
 %% Output
 
     $1$
     1
 
 %% Cell type:code id: tags:
 
 ``` prob
 ∅ : {∅}
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:markdown id: tags:
 
 Die Notation `{x | P}` wobei eine Menge per Prädikat definiert wird ist die mächtigste Notation.
 
 %% Cell type:code id: tags:
 
 ``` prob
 {x | x>1 & x<1  }
 ```
 
 %% Output
 
     $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
     ∅
 
 %% Cell type:code id: tags:
 
 ``` prob
  {x | x=1 or x=2 }
 ```
 
 %% Output
 
     $\{1,2\}$
     {1,2}
 
 %% Cell type:code id: tags:
 
 ``` prob
 {x | x>=1 & x<=4 }
 ```
 
 %% Output
 
     $\{1,2,3,4\}$
     {1,2,3,4}
 
 %% Cell type:code id: tags:
 
 ``` prob
 NAT = {x | x>=0 }
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:markdown id: tags:
 
 In Event-B gibt es auch eine angepasste Variante der Notation `{x . P | E}`, wo man einen Ausdruck `E` angibt der in die generierte Menge eingefügt wird:
 
 %% Cell type:code id: tags:
 
 ``` prob
 {x.x:1..10|x*x}
 ```
 
 %% Output
 
     $\{1,4,9,16,25,36,49,64,81,100\}$
     {1,4,9,16,25,36,49,64,81,100}
 
 %% Cell type:markdown id: tags:
 
 ## Prädikate über Mengen
 
 Es gibt die Standardprädikate der Mathematik:
 * ∈
 * ∉
 * ⊆
 * ⊂
 
 %% Cell type:code id: tags:
 
 ``` prob
 :prettyprint not({1,2,3} /<<: {1,2,3})
 ```
 
 %% Output
 
     $\neg (\{1,2,3\} \not\subset  \{1,2,3\})$
     ¬({1,2,3} ⊄ {1,2,3})
 
 %% Cell type:markdown id: tags:
 
 Zusätzlich hat Event-B das partition Prädikat, welches wir weiter unter erklären.
 
 %% Cell type:markdown id: tags:
 
 ## Operatoren über Mengen
 
 * Vereinigung         \/   ∪
 * Schnittmenge      /\   ∩
 * Differenzmenge    \
 * union(S), inter(S) für Menge von Mengen
 * POW(S) (Potenzmenge: Untermengen von S)
 * POW1(S) (nicht leeren Untermengen von S)
 
 Übung: diese Operatoren durch comprehension sets definieren
 
 %% Cell type:code id: tags:
 
 ``` prob
 a = {1,2,4} & b = {2,3,4} & aub1 = a \/ b &
 aub2 = {x | x:a or x:b}
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{a} = \{1,2,4\}$
     * $\mathit{b} = \{2,3,4\}$
     * $\mathit{aub2} = \{1,2,3,4\}$
     * $\mathit{aub1} = \{1,2,3,4\}$
     TRUE
     
     Solution:
     	a = {1,2,4}
     	b = {2,3,4}
     	aub2 = {1,2,3,4}
     	aub1 = {1,2,3,4}
 
 %% Cell type:code id: tags:
 
 ``` prob
 a = {1,2,4} & b = {2,3,4} & aib1 = a/\b &
 aib2 = {x | x:a & x:b}
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{a} = \{1,2,4\}$
     * $\mathit{b} = \{2,3,4\}$
     * $\mathit{aib2} = \{2,4\}$
     * $\mathit{aib1} = \{2,4\}$
     TRUE
     
     Solution:
     	a = {1,2,4}
     	b = {2,3,4}
     	aib2 = {2,4}
     	aib1 = {2,4}
 
 %% Cell type:code id: tags:
 
 ``` prob
 a = {1,2,4} & b = {2,3,4} & aib1 = a \ b
 & aib2 = {x | x:a & x/:b}
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{a} = \{1,2,4\}$
     * $\mathit{b} = \{2,3,4\}$
     * $\mathit{aib2} = \{1\}$
     * $\mathit{aib1} = \{1\}$
     TRUE
     
     Solution:
     	a = {1,2,4}
     	b = {2,3,4}
     	aib2 = {1}
     	aib1 = {1}
 
 %% Cell type:code id: tags:
 
 ``` prob
 {x.x:1..10|x*x}
 ```
 
 %% Output
 
     $\{1,4,9,16,25,36,49,64,81,100\}$
     {1,4,9,16,25,36,49,64,81,100}
 
 %% Cell type:code id: tags:
 
 ``` prob
 a = {1,2,4} & b = {2,3,4} & c = {4,6} & abc = union({a,b,c})
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{a} = \{1,2,4\}$
     * $\mathit{b} = \{2,3,4\}$
     * $\mathit{c} = \{4,6\}$
     * $\mathit{abc} = \{1,2,3,4,6\}$
     TRUE
     
     Solution:
     	a = {1,2,4}
     	b = {2,3,4}
     	c = {4,6}
     	abc = {1,2,3,4,6}
 
 %% Cell type:code id: tags:
 
 ``` prob
 POW(1..2)
 ```
 
 %% Output
 
     $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{1\},\{1,2\},\{2\}\}$
     {∅,{1},{1,2},{2}}
 
 %% Cell type:code id: tags:
 
 ``` prob
 POW(BOOL)
 ```
 
 %% Output
 
     $\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\}$
     {∅,{FALSE},{FALSE,TRUE},{TRUE}}
 
 %% Cell type:code id: tags:
 
 ``` prob
 POW(POW(BOOL))
 ```
 
 %% Output
 
     $\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\renewcommand{\emptyset}{\mathord\varnothing}\{\emptyset,\{\emptyset\},\{\emptyset,\{\mathit{FALSE}\}\},\{\emptyset,\{\mathit{FALSE},\mathit{TRUE}\}\},\{\emptyset,\{\mathit{TRUE}\}\},\{\{\mathit{FALSE}\}\},\{\emptyset,\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\}\},\{\emptyset,\{\mathit{FALSE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\}\},\{\{\mathit{FALSE}\},\{\mathit{TRUE}\}\},\{\emptyset,\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE},\mathit{TRUE}\}\},\{\emptyset,\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE}\},\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{FALSE},\mathit{TRUE}\},\{\mathit{TRUE}\}\},\{\{\mathit{TRUE}\}\}\}$
     {∅,{∅},{∅,{FALSE}},{∅,{FALSE,TRUE}},{∅,{TRUE}},{{FALSE}},{∅,{FALSE},{FALSE,TRUE}},{∅,{FALSE},{TRUE}},{{FALSE},{FALSE,TRUE}},{{FALSE},{TRUE}},{∅,{FALSE},{FALSE,TRUE},{TRUE}},{{FALSE,TRUE}},{∅,{FALSE,TRUE},{TRUE}},{{FALSE},{FALSE,TRUE},{TRUE}},{{FALSE,TRUE},{TRUE}},{{TRUE}}}
 
 %% Cell type:code id: tags:
 
 ``` prob
 card(POW(POW(POW(BOOL))))
 ```
 
 %% Output
 
     $65536$
     65536
 
 %% Cell type:markdown id: tags:
 
 ## Übung: Send More Money
 
 Man soll 8 Ziffern finden so dass folgende Summe aufgeht
 
 |   |   |   |   |   |   |
 |---|---|---|---|---|---|
 |   |   | S | E | N | D |
 |   | + | M | O | R | E |
 | = | M | O | N | E | Y |
 
 Wir brauchen acht Ziffern:
 
 %% Cell type:code id: tags:
 
 ``` prob
 {S,E,N,D,M,O,R,Y}<:0..9
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{R} = 0$
     * $\mathit{S} = 0$
     * $\mathit{D} = 0$
     * $\mathit{E} = 0$
     * $\mathit{Y} = 0$
     * $\mathit{M} = 0$
     * $\mathit{N} = 0$
     * $\mathit{O} = 0$
     TRUE
     
     Solution:
     	R = 0
     	S = 0
     	D = 0
     	E = 0
     	Y = 0
     	M = 0
     	N = 0
     	O = 0
 
 %% Cell type:markdown id: tags:
 
 Diese Ziffern sollen alle unterschiedlich sein:
 
 %% Cell type:code id: tags:
 
 ``` prob
 {S,E,N,D,M,O,R,Y}⊆0..9 & card({S,E,N,D,M,O,R,Y}) = 8
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{R} = 2$
     * $\mathit{S} = 0$
     * $\mathit{D} = 5$
     * $\mathit{E} = 7$
     * $\mathit{Y} = 1$
     * $\mathit{M} = 4$
     * $\mathit{N} = 6$
     * $\mathit{O} = 3$
     TRUE
     
     Solution:
     	R = 2
     	S = 0
     	D = 5
     	E = 7
     	Y = 1
     	M = 4
     	N = 6
     	O = 3
 
 %% Cell type:markdown id: tags:
 
 Die Ziffern S und M dürfen nicht 0 sein:
 
 %% Cell type:code id: tags:
 
 ``` prob
 {S,E,N,D,M,O,R,Y}⊆0..9 & card({S,E,N,D,M,O,R,Y}) = 8 &
 S /= 0 & M /= 0
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{R} = 3$
     * $\mathit{S} = 2$
     * $\mathit{D} = 5$
     * $\mathit{E} = 7$
     * $\mathit{Y} = 0$
     * $\mathit{M} = 1$
     * $\mathit{N} = 6$
     * $\mathit{O} = 4$
     TRUE
     
     Solution:
     	R = 3
     	S = 2
     	D = 5
     	E = 7
     	Y = 0
     	M = 1
     	N = 6
     	O = 4
 
 %% Cell type:markdown id: tags:
 
 Und jetzt muss noch die Summe stimmen:
 
 %% Cell type:code id: tags:
 
 ``` prob
 {S,E,N,D,M,O,R,Y}<:0..9 & card({S,E,N,D,M,O,R,Y}) = 8 &
 S /= 0 & M /= 0 &
 S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E =
 M*10000 + O*1000 + N*100 + E*10 + Y
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{R} = 8$
     * $\mathit{S} = 9$
     * $\mathit{D} = 7$
     * $\mathit{E} = 5$
     * $\mathit{Y} = 2$
     * $\mathit{M} = 1$
     * $\mathit{N} = 6$
     * $\mathit{O} = 0$
     TRUE
     
     Solution:
     	R = 8
     	S = 9
     	D = 7
     	E = 5
     	Y = 2
     	M = 1
     	N = 6
     	O = 0
 
 %% Cell type:markdown id: tags:
 
 Wir können auch die Menge aller Lösungen bestimmen:
 
 %% Cell type:code id: tags:
 
 ``` prob
 :table {S|->E|->N|->D|->M|->O|->R|->Y |
   {S,E,N,D,M,O,R,Y}⊆0..9 & card({S,E,N,D,M,O,R,Y}) = 8 &
    S /= 0 & M /= 0 &
    S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E
    = M*10000 + O*1000 + N*100 + E*10 + Y }
 ```
 
 %% Output
 
     |S|E|N|D|M|O|R|Y|
     |---|---|---|---|---|---|---|---|
     |9|5|6|7|1|0|8|2|
     S	E	N	D	M	O	R	Y
     9	5	6	7	1	0	8	2
 
 %% Cell type:markdown id: tags:
 
 ## Das Partition Prädikat
 
 Dieses Prädikat gibt es nur in Event-B und es ist syntaktischer Zucker für einen grösseren äquivalenten Ausdruck:
 ```
  partition(S,S1,S2,...,Sn)
  ```
  steht für
  ```
    S = S1 \/ S2 \/ ... Sn &
    S1 /\ S2 = {} & ... S1 /\ Sn = {} &
    S2 /\ S3 = {} & ... S2 /\ Sn = {}
    ...
    Sn-1 /\ Sn = {}
    ```
 
 %% Cell type:code id: tags:
 
 ``` prob
 :language event_b
 ```
 
 %% Output
 
     Changed language for user input to Event-B (forced)
 
 %% Cell type:code id: tags:
 
 ``` prob
 partition(1..3,{1},{2},{3})
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 :table {a|->b| partition(1..2,a,b)}
 ```
 
 %% Output
 
     |a|b|
     |---|---|
     |∅|{1,2}|
     |{1}|{2}|
     |{1,2}|∅|
     |{2}|{1}|
     a	b
     {}	{1,2}
     {1}	{2}
     {1,2}	{}
     {2}	{1}
 
 %% Cell type:markdown id: tags:
 
 ## Neue Basismengen
 
 Vom Benutzer können in Event-B neue Basismengen eingeführt werden
 
 * werden in der `sets` Sektion von Kontexten eingeführt
 * jede Benutzermenge ist sein eigener Typ!
 
 Man darf unterschiedliche Mengen bzw. Elemente aus unterschiedlichen Basismengen nicht mischen.
 
 Es gibt zwei Möglichkeiten:
 1) Enumerated Set: man gibt explizit alle Elemente der neuen Basismenge an
 S = {a,b,c} in klassischem B oder partition(S,{a},{b},{c}).
 2) Deferred Set: man lässt die Menge für Erweiterungen offen
 
 In Rodin gibt es zwei Wizards zum einführen von enumerated bzw. deferred "carrier" sets.
 
 %% Cell type:markdown id: tags:
 
 ## Typen in B
 
 * es gibt einen Typ für alle Zahlen: INT (ℤ)
 * es gibt den Typ BOOL für die Bool'schen Werte
 * für jede Basismenge gibt es einen eigenen Typen
 * ist t ein Typ, dann ist POW(t) auch ein Typ
 * nächste Woche werden wir noch ein weitere Typkonstruktion sehen
 
 Jeder Ausdruck und damit auch jede Variable muss genau einen Typen haben. Die Typen müssen mit den Signaturen der B Operatoren kompatibel sein.
 
 * man kann explizit Typen angeben, mit einem Prädikat `VARIABLE ∈ TYP`, zum Beispiel: `a∈ℤ`
 * oder auf die Typ-Inferenz von Atelier-B, Rodin, ProB hoffen (Atelier-B am schwächsten; ProB am mächtigsten)
 
 Beispiele:
 
 %% Cell type:code id: tags:
 
 ``` prob
 :type 1
 ```
 
 %% Output
 
     INT
 
 %% Cell type:code id: tags:
 
 ``` prob
 1 ∈ ℤ
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 :type {1}
 ```
 
 %% Output
 
     POW(INT)
 
 %% Cell type:code id: tags:
 
 ``` prob
 {1} ∈ POW(INT)
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 NAT : POW(INT)
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     TRUE
 
 %% Cell type:code id: tags:
 
 ``` prob
 :type {}
 ```
 
 %% Output
 
     POW(?)
 
 %% Cell type:markdown id: tags:
 
 Are the following two expressions well-typed? What are the type inference rules?
 
 %% Cell type:code id: tags:
 
 ``` prob
 1+card({TRUE})
 ```
 
 %% Output
 
     $2$
     2
 
 %% Cell type:code id: tags:
 
 ``` prob
 {TRUE} ∪ {1}
 ```
 
 %% Output
 
     de.prob.exception.CliError: Exception while processing command result
 
 %% Cell type:markdown id: tags:
 
 ### Inferenzregeln für Typen
 
 Folgende Regeln sind relevant um die Typen der beiden Ausdrücke oben zu prüfen:
 
 * type(1) = INTEGER
 * type(TRUE) = BOOL
 * type({ x }) = POW(XT)  where type(x) = XT
 * type(a+b) = INTEGER if type(a)=type(b)=INTEGER
 * type(a ∪ b) = POW(T)  if type(a) = type(b) = POW(T)
 
 
 %% Cell type:markdown id: tags:
 
 # Kleine Beispiele
 
 %% Cell type:code id: tags:
 
 ``` prob
 1+x=3
 ```
 
 %% Output
 
     $\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{x} = 2$
     TRUE
     
     Solution:
     	x = 2
 
 %% Cell type:code id: tags:
 
 ``` prob
 :language event_b
 ```
 
 %% Output
 
     Changed language for user input to Event-B (forced)
 
 %% Cell type:markdown id: tags:
 
 Wenn man die Menge der Primzahlen so definiert, behält ProB diese als symbolische Menge:
 
 %% Cell type:code id: tags:
 
 ``` prob
 Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)}
 ```
 
 %% Output
 
     $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{Primzahlen} = /*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \forall\mathit{y}\qdot(\mathit{y} \in 2 \upto \mathit{x} - 1 \limp \mathit{x} \mathit{mod} \mathit{y} > 0)\}$
     TRUE
     
     Solution:
     	Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}
 
 %% Cell type:markdown id: tags:
 
 Man kann aber zum Beispiel eine Primzahl generieren:
 
 %% Cell type:code id: tags:
 
 ``` prob
 x∈Primzahlen ∧ Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)}
 ```
 
 %% Output
 
     $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{x} = 2$
     * $\mathit{Primzahlen} = /*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \forall\mathit{y}\qdot(\mathit{y} \in 2 \upto \mathit{x} - 1 \limp \mathit{x} \mathit{mod} \mathit{y} > 0)\}$
     TRUE
     
     Solution:
     	x = 2
     	Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}
 
 %% Cell type:markdown id: tags:
 
 Man kann die Menge der Primzahlen auch mit 1..100 schneiden um die Primzahlen bis 100 zu bekommen:
 
 %% Cell type:code id: tags:
 
 ``` prob
 Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} ∧
 res = Primzahlen ∩ 1..100
 ```
 
 %% Output
 
     $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{res} = \{2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97\}$
     * $\mathit{Primzahlen} = /*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \forall\mathit{y}\qdot(\mathit{y} \in 2 \upto \mathit{x} - 1 \limp \mathit{x} \mathit{mod} \mathit{y} > 0)\}$
     TRUE
     
     Solution:
     	res = {2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97}
     	Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}
 
 %% Cell type:markdown id: tags:
 
 Hier rechnen wir jetzt die Anzahl der Primzahle bis 1000 aus:
 
 %% Cell type:code id: tags:
 
 ``` prob
 Primzahlen = {x|x>1 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)} ∧
 res = card(Primzahlen ∩ 1..1000)
 ```
 
 %% Output
 
     $\newcommand{\qdot}{\mathord{\mkern1mu\cdot\mkern1mu}}\newcommand{\upto}{\mathbin{.\mkern1mu.}}\newcommand{\limp}{\mathbin\Rightarrow}\mathit{TRUE}$
     
     **Solution:**
     * $\mathit{res} = 168$
     * $\mathit{Primzahlen} = /*@\mathit{symbolic}*/ \{\mathit{x}\mid\mathit{x} > 1 \land \forall\mathit{y}\qdot(\mathit{y} \in 2 \upto \mathit{x} - 1 \limp \mathit{x} \mathit{mod} \mathit{y} > 0)\}$
     TRUE
     
     Solution:
     	res = 168
     	Primzahlen = /*@symbolic*/ {x∣x > 1 ∧ ∀y·(y ∈ 2 ‥ x − 1 ⇒ x mod y > 0)}
 
 %% Cell type:code id: tags:
 
 ``` prob
 :table {x|x:1..20 ∧ ∀y.(y∈2..(x-1) ⇒ x mod y > 0)}
 ```
 
 %% Output
 
     |x|
     |---|
     |1|
     |2|
     |3|
     |5|
     |7|
     |11|
     |13|
     |17|
     |19|
     x
     1
     2
     3
     5
     7
     11
     13
     17
     19
 
 %% Cell type:code id: tags:
 
 ``` prob
 ```