add formula generation

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

add formula generation
ef399951 · Michael Leuschel · f5db25b0 · ef399951
Commit ef399951 authored 2 years ago by Michael Leuschel
--- a/logic_programming/3_PropositionalLogic.ipynb
+++ b/logic_programming/3_PropositionalLogic.ipynb
@@ -1665,9 +1665,27 @@
    "jupyter:retry."
   ]
  },
+  {
+   "cell_type": "markdown",
+   "id": "35fba4c7",
+   "metadata": {},
+   "source": [
+    "### Appendix: Generating equivalent formulas"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "78beaf88",
+   "metadata": {},
+   "source": [
+    "The code below can be used to generate formulas in Prolog using a technique similar to iterative deepening.\n",
+    "We will study this technique much later in the course in the lectures on search.\n",
+    "All you need to know is that generate_formula generates formulas from smaller to deeper formulas."
+   ]
+  },
  {
   "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 55,
   "id": "51d5630b",
   "metadata": {
    "vscode": {
@@ -1675,6 +1693,210 @@
    }
   },
   "outputs": [],
+   "source": [
+    "generate_formula(X) :- \n",
+    "   peano(MaxDepth), gen(X,MaxDepth).\n",
+    "peano(0).\n",
+    "peano(s(X)) :- peano(X).\n",
+    "\n",
+    "proposition(p).\n",
+    "proposition(q).\n",
+    "proposition(r).\n",
+    "\n",
+    "gen(X,_) :- proposition(X).\n",
+    "gen(and(A,B),s(MaxDepth)) :- gen(A,MaxDepth), gen(B,MaxDepth).\n",
+    "gen(or(A,B),s(MaxDepth)) :- gen(A,MaxDepth), gen(B,MaxDepth).\n",
+    "gen(implies(A,B),s(MaxDepth)) :- gen(A,MaxDepth), gen(B,MaxDepth).\n",
+    "gen(equiv(A,B),s(MaxDepth)) :- gen(A,MaxDepth), gen(B,MaxDepth).\n",
+    "gen(not(A),s(MaxDepth)) :- gen(A,MaxDepth)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 56,
+   "id": "f843534d",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mX = p"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?-generate_formula(X)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 57,
+   "id": "3e0e951d",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mX = q"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:retry."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 58,
+   "id": "8199e19a",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mX = r"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:retry."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "cd56c6d2",
+   "metadata": {},
+   "source": [
+    "We can now use this together with our other Prolog predicates to generate equivalent formulas:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 60,
+   "id": "fae03e15",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mFormula = and(q,p)"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- generate_formula(Formula), equivalent(and(p,q),Formula), Formula \\= and(p,q)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 61,
+   "id": "94b16168",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mFormula = and(p,and(p,q))"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:retry."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 62,
+   "id": "a49ecd78",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mFormula = p"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- generate_formula(Formula), equivalent(and(p,p),Formula)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 63,
+   "id": "49caff90",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mFormula = p"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- generate_formula(Formula), equivalent(and(p,or(p,q)),Formula)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "79db3ffb",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
   "source": []
  }
 ],

 %% 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.
 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, ")".
 ```
 %% Cell type:code id:fc6823ad tags:
 ``` prolog
 ?- wff("p","").
 ```
 %% Output
 %% Cell type:code id:152289b6 tags:
 ``` prolog
 ?- wff("(¬p)","").
 ```
 %% Output
 %% Cell type:code id:2c3dd1bf tags:
 ``` prolog
 ?- 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.
 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
 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), ")".
 ```
 %% Cell type:code id:8ddb568d tags:
 ``` prolog
 ?- wff(Formula,"(¬p)","").
 ```
 %% Output
 %% Cell type:code id:075dc3b2 tags:
 ``` prolog
 ?- wff(Formula,"(¬(p∧q))","").
 ```
 %% Output
 %% Cell type:code id:338cb7dd tags:
 ``` prolog
 ?- wff(Formula,"(p∧(q∨(¬p)))","").
 ```
 %% 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(_,_,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`.
 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).
 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).
 ```
 %% 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))
 ```
 %% Output
    A | B | NotA | AandB | AorB | AimpliesB | AequivB |
    :- | :- | :- | :- | :- | :- | :- |
    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:
 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:8f6d804b tags:
 ``` prolog
 ?- Interpetation=[p/true, q/false],  member(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:eee17774 tags:
 ``` prolog
 ?- value(and(p,or(q,not(p))), [p/true, q/false],Res).
 ```
 %% Output
 %% Cell type:markdown id:4387b4a2 tags:
 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: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
   functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect),
   (value(Sub,Interpretation,true) -> C=olive ; C=sienna1).
 ```
 %% 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:
 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:
 Two formulas are called <b>equivalent</b> iff they have the same models:
 %% Cell type:code id:b912acd3 tags:
 ``` prolog
 jupyter:print_table(value(or(not(p),q), [p/P, q/Q],Res))
 ```
 %% Output
    P | Q | Res |
    :- | :- | :- |
    true | true | true |
    true | false | false |
    false | true | true |
    false | false | true |
 %% Cell type:code id:f4c9823d tags:
 ``` prolog
 jupyter:print_table(value(implies(p,q), [p/P, q/Q],Res))
 ```
 %% Output
    P | Q | Res |
    :- | :- | :- |
    true | true | true |
    true | false | false |
    false | true | true |
    false | false | true |
 %% Cell type:code id:68a2a19c tags:
 ``` prolog
 jupyter:print_table((user:value(or(not(p),q), [p/P, q/Q],NotPandQ),user:value(implies(p,q), [p/P, q/Q],PimpliesQ)))
 ```
 %% Output
    P | Q | NotPandQ | PimpliesQ |
    :- | :- | :- | :- |
    true | true | true | true |
    true | false | false | false |
    false | true | true | true |
    false | false | true | true |
 %% Cell type:markdown id:248d3d32 tags:
 A formula `B` is the logical consequence of `A` if all models of `A` are also models of `B`:
 %% 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
 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: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: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:code id:f552a71e tags:
 ``` prolog
 ?- prove(and(p,q),or(p,q)).
 ```
 %% Output
 %% Cell type:code id:f8aca8b7 tags:
 ``` prolog
 ?- equivalent(and(p,q),or(p,q)).
 ```
 %% Output
 %% Cell type:code id:e7a2828d tags:
 ``` prolog
 ?- prove(or(p,q),and(p,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: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:
 %% 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: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.
 %% 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).
 ```
 %% Output
 %% Cell type:code id:0919b40c tags:
 ``` prolog
 jupyter:retry.
 ```
 %% 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:code id:79db3ffb tags:
+``` prolog
 ```