vault backup: 2023-11-14 11:32:32

.obsidian/core-plugins.json

@@ -1,20 +0,0 @@
-[
-  "file-explorer",
-  "global-search",
-  "switcher",
-  "graph",
-  "backlink",
-  "canvas",
-  "outgoing-link",
-  "tag-pane",
-  "page-preview",
-  "daily-notes",
-  "templates",
-  "note-composer",
-  "command-palette",
-  "editor-status",
-  "bookmarks",
-  "outline",
-  "word-count",
-  "file-recovery"
-]

.obsidian/workspace.json

@@ -4,28 +4,16 @@
     "type": "split",
     "children": [
       {
-        "id": "c0bba0acc3e22afb",
+        "id": "e1841f20d0865df6",
         "type": "tabs",
         "children": [
           {
-            "id": "9853b375f7893cb9",
+            "id": "a3f61b3a67420afc",
             "type": "leaf",
             "state": {
               "type": "markdown",
               "state": {
-                "file": "4a1s/MFES/PL - Aula 4.md",
-                "mode": "source",
-                "source": false
-              }
-            }
-          },
-          {
-            "id": "47ffa0ada12cc565",
-            "type": "leaf",
-            "state": {
-              "type": "markdown",
-              "state": {
-                "file": "4a1s/MFES/PL - Aula 6.md",
+                "file": "4a1s/MFES/PL - Aula 8.md",
                 "mode": "source",
                 "source": false
               }
@@ -97,7 +85,7 @@
             "state": {
               "type": "backlink",
               "state": {
-                "file": "4a1s/MFES/PL - Aula 4.md",
+                "file": "4a1s/MFES/PL - Aula 8.md",
                 "collapseAll": false,
                 "extraContext": false,
                 "sortOrder": "alphabetical",
@@ -114,7 +102,7 @@
             "state": {
               "type": "outgoing-link",
               "state": {
-                "file": "4a1s/MFES/PL - Aula 4.md",
+                "file": "4a1s/MFES/PL - Aula 8.md",
                 "linksCollapsed": false,
                 "unlinkedCollapsed": true
               }
@@ -137,7 +125,7 @@
             "state": {
               "type": "outline",
               "state": {
-                "file": "4a1s/MFES/PL - Aula 4.md"
+                "file": "4a1s/MFES/PL - Aula 8.md"
               }
             }
           },
@@ -170,10 +158,12 @@
       "digitalgarden:Digital Garden Publication Center": false
     }
   },
-  "active": "9853b375f7893cb9",
+  "active": "a3f61b3a67420afc",
   "lastOpenFiles": [
-    "4a1s/MFES/PL - Aula 3.md",
+    "4a1s/MFES/PL - Aula 8.md",
     "4a1s/MFES/PL - Aula 4.md",
+    "4a1s/MFES/MFES - UC Details.md",
+    "4a1s/MFES/PL - Aula 3.md",
     "4a1s/MFES/PL - Aula 5.md",
     "4a1s/MFES/PL - Aula 7.md",
     "4a1s/index.md",
@@ -196,9 +186,7 @@
     "Excalidraw/doodles.excalidraw.md",
     "My Digital Garden.md",
     "4a1s/MFES/T - Aula 2.md",
-    "4a1s/MFES/PL - Aula 2.md",
     "Images/Pasted image 20231018122801.png",
-    "Excalidraw/Drawing 2023-10-25 12.16.38.excalidraw.md",
     "Images/Pasted image 20231018121319.png",
     "Images/Pasted image 20231018120412.png",
     "Images/Pasted image 20231018120219.png",

4a1s/MFES/PL - Aula 8.md

@@ -0,0 +1,115 @@
+https://why3.lri.fr/try/?name=test.mlw&lang=whyml&code=AN7HpJ4Recall1the4officeyassignment%2F4puzzle2from3Fichaz17r3whereBHz44people1areydistributed%2F0byz35officesl2such2that7vH7s2each4person0is6assignedza4singleVHm2Nuno1and3Pedro0do1not3share0anlHl0If1Ana1hasoo2just1for5herselfV2then0so2doesdHg5Officesyaccomodate%2F0at2most1twouIHHuBuMg0if5running2Why32withXyappropriate%2F1SMT4solverlBH0inuByfollowing%2F1you2will0be2able0to5inspect5counterASA6examplesBH2when6adequate7tBNHHz1s3Modele5problemuI6definingVVypredicate%2FBKuQ5writingza1set0of4axiomsfH0In3orderV5expressc3thirdyrequirement%2F3above7r4defineBHfc7h3alonesyexpressing%2Ful5someoneuMg2onlyBH6occupierXSuVWHEz2s2ShowikTuGuPyinconsistent%2Fu0u3hBKu12goalhHEz3s2Find1outuhfunyproperties%2F4followuDpb7vL7suP3MariaPuKR1One7ruT1sheukukLfu7u7u7u8iTDccuOusuLuMu9lbbXmuSaBL5equally2haveusiiidBMDHz4s5Finallyfyformulate%2Fg3provezau85statingVBLuUuU1onef1mayvG3emptyd1For2thisc3first3writeduvBHuwdVfvAg7nzieAzesuzu%2FvO4anyone7ItBHDz5n5Producefyalternative%2Fyformalization%2F3usingV5insteadvEVVpBLr3logic6functionU3givesvB4uniqueRXXBHuIuIY4Repeat1allk6previous3stepsuXvWVlDN7JoBNNNN4moduleuQNF2typec7yu7781Twos3ThreeHnanu%2Fou%2FsvBsvANHveyhasOffice%2F7nk7orerNH3axiom0A1B7v4forallzprAlV4existszopAjphmoHj0A2BmjorAj7r0o10o2BphhJhln7O3qqm7MzoUqFHfzBBiBfnoqhhiVngqUlgLo7RzqDHVurUbfAZUZbWAoAaap0p1plpJjbikiapkpbngpNFXzCgdPlrWHnzDBnBbk0p20p3ApZRdqXXJakoZqjqqqjqdLnam7XuqqnqsrpNMBvHysanity%2Btest%2Fg3falseuAA3checkuzvk3model3makes3senseAvpHHi0g1BiBZvvvrYv3qHm0g2mPvyrQQ7nhv1nOqvxq7oeBLvvvxAhAhhkvyoiqcqBNDvxvQdzoiif7yazpAoAvxdvQjenijHH3lemmayatMostOneEmpty%2FBjBiXcqBegdoarnXLpbqNN1endBNNNNvnyOffices%2BFn%2FBNDvqinv978vosvoHnTnv%2Bov%2BsOsONHvZhPkSVBpNHvqzBqqjvprhHHv8v4izplAhhcOzooAi7tpvpplpJqfjOlrqrpHFbzCkeWkraNHnzDnBfkvrvqpddoAeAnv8qAqAmqpAqAqgLdnprovprpBpBrnNNDv0vpBhBvpBNHqvxBqnOUv9fXpHlvxBllVkrOkrlprUNHOv27nOiAn7olRzpAoAQQmpUkHHv0v0Blkv0v0qkjeov8rnZLpeqNNv0NNNN
+```c
+(*
+    Recall the office assignment puzzle from Ficha 1, where 
+    4 people are distributed by 3 offices, such that:
+    - each person is assigned a single office
+    - Nuno and Pedro do not share an office
+    - If Ana has an office just for herself, then so does Pedro
+    - Offices accomodate at most two people
+    
+    Recall that, if running Why3 with an appropriate SMT solver, 
+    in the following you will be able to inspect counter-examples 
+    when adequate. 
+
+    
+    1. Model the problem by defining an appropriate predicate 
+       and writing a set of axioms.
+       In order to express the third requirement above, define 
+       a predicate "alone" expressing that someone is the only 
+       occupier of an office.
+       
+    2. Show that the axioms are not inconsistent by writing an 
+       appropriate goal.
+       
+    3. Find out if the following properties follow from the axioms:
+        - If Maria is assigned office One, then she will be
+            the only occupier of that office.
+        - If Ana and Nuno share an office, then Maria and Pedro will 
+            equally have to share an office. 
+    
+    4. Finally, formulate and prove a goal stating that 
+        at most one office may be empty. For this, first write a predicate 
+        expressing that an office is empty (i.e. not assigned to anyone). 
+        
+    5. Produce an alternative formalization using, instead of a predicate, 
+        a logic function that gives the unique office assigned to 
+        each person. Repeat all the previous steps with this formalization.
+    
+*) 
+
+
+
+module Offices
+
+  type office = One | Two | Three
+  type person = Ana | Nuno | Pedro | Maria
+
+  predicate hasOffice (person) (office)
+
+  axiom A1 : forall p:person. exists o:office. hasOffice p o
+  axiom A2 : forall p:person, o1 o2 : office.
+    hasOffice p o1 /\ hasOffice p o2 -> o1 = o2
+  
+  axiom B : forall o1 o2 : office. hasOffice Pedro o1 /\ hasOffice Nuno o2 ->
+      o1 <> o2
+  
+  predicate alone (p:person) = forall o:office. forall p1:person.
+    (hasOffice p o) /\ hasOffice p1 o -> p = p1
+
+  axiom C : alone Ana -> alone Pedro
+  axiom D : forall p1 p2 p3: person, o:office.
+    hasOffice p1 o /\ hasOffice p2 o /\ hasOffice p3 o ->
+        p1 = p2 \/ p1 = p3 \/ p3 = p2
+
+  goal sanity_test : false (*check if the model makes sense*)
+  
+  goal g1 : hasOffice Maria One -> alone Maria
+  goal g2 : forall o1:office. (hasOffice Ana o1 /\ hasOffice Nuno o1) -> 
+      exists o2:office. hasOffice Pedro o2 /\ hasOffice Maria o2 
+
+  predicate empty (o:office) = forall p:person. not (hasOffice p o)
+  
+  lemma atMostOneEmpty : forall o1 o2: office. empty o1 /\ empty o2 ->
+      o1 = o2
+
+end 
+
+
+
+
+
+
+
+module Offices_Fn 
+
+  type office = One | Two | Three
+  type person = Ana | Nuno | Pedro | Maria
+
+  function office (person) : office
+
+  axiom B: office Pedro <> office Nuno
+  
+  predicate alone (p:person) = forall o:office. forall p1:person.
+    p1 <> p -> office p <> office p1
+    
+  axiom C: alone Ana -> alone Pedro
+
+  axiom D: forall p1 p2 p3: person. p1<>p2 /\ p1<>p3 /\ p2<>p3 ->
+      office p1 <> office p2 \/ office p1 <> office p3
+
+
+  goal sanity_test : false 
+
+  goal g1 : office Maria = One -> alone Maria
+  goal g2 : office Ana = office Nuno -> office Maria = office Pedro
+
+  predicate empty (o:office) = forall p:person. office p <> o
+  
+  lemma atMostOneEmpty : forall o1 o2: office. empty o1 /\ empty o2 ->
+      o1 = o2
+
+end
+```
+
+