vault backup: 2023-09-19 12:13:41

.obsidian/workspace.json

@@ -150,15 +150,15 @@
       "obsidian-excalidraw-plugin:Create new drawing": false
     }
   },
-  "active": "4c008c59a631fa8d",
+  "active": "201fe1705c33e116",
   "lastOpenFiles": [
-    "Notes/MFES/MFES - UC Details.md",
     "README.md",
+    "Notes/MFES/T - Aula 2 - 18 Setembro 2023.md",
+    "Notes/MFES/MFES - UC Details.md",
     "2023-09-18.md",
     "MFES/T - Aula 2 - 18 Setembro 2023.md",
     "Notes/RAS/T - Aula 2 - 19 Setembro 2023.md",
     "Notes/RAS",
-    "Notes/MFES/T - Aula 2 - 18 Setembro 2023.md",
     "Notes/MFES",
     "Notes",
     "RAS/T - Aula 2 - 19 Setembro 2023.md",

Notes/MFES/T - Aula 2 - 18 Setembro 2023.md

@@ -1,9 +1,9 @@
-# Intro
+# 1. Intro
 *Formal modeling* - formally represent the system and its properties in the syntactic conventions that the tool understands and can process. 
 
 Formal Logic = logical language (logical symbols + non-logical symbols) + semantics +proof system
 
-### SAT
+### 1.1 SAT
 <iframe title="Boolean Satisfiability Problem - Intro to Theoretical Computer Science" src="https://www.youtube.com/embed/uAdVzz1hKYY?feature=oembed" height="113" width="200" allowfullscreen="" allow="fullscreen" style="aspect-ratio: 1.76991 / 1; width: 100%; height: 100%;"></iframe>
 
 The Boolean satisfiability (SAT) problem:
@@ -25,7 +25,14 @@ Usually SAT solvers deal with formulas in conjunctive normal form (CNF)
  > SAT is NP-complete
 
 
-## Proposicional Logic (PL)
+## 1.2 Proposicional Logic (PL)
+
+>[!note] Nota
+>Esta secção basicamente só contém revisão de conceitos. Aconselha-se a ver a coisa rapidamente, porque é só a formalidade de lógica escrita por extenso.
+
+Let $A$ be an assignment and let $F$ be a formula. If $A(F) = 1$, then we say **$F$ holds under assignment**, or **$A$ models $F$.**
+We write A $\models F$ iff $A(F)=1$, and $A \not \models F$ iff $A(F) = 0$.
+
 
 An assignment is a function $A$ : $V_{prop} \implies {0,1}$  , that assigns to every
 propositional variable a truth value. An assignment $A$ naturally extends to all formulas, $A$ : **Form** $\implies {0,1}$. The truth value of a formula is computed using **truth tables**:
@@ -40,5 +47,45 @@ propositional variable a truth value. An assignment $A$ naturally extends to all
 
 
 A formula $F$ is:
-1. **valid**  iff it holds under every assignment. We write $F$
+1. **valid**  iff it holds under every assignment. We write $\models F$. A valid formula is called a *tautology*.
+2. **satisfiable** iff it folds (true) under some assignment.
+3. **unsatisfiable** iff it holds under no assignment. An unsatisfiable formula is called a *contradiction*.
+4. **refutable** iff it is not valid.
+
+   > [!tip]+ Proposition
+   >  $F$ is **valid** iff $\neg F$ is **unsatisfiable**.
+   
+
+- $F \models G$ iff for every assignment $A$, if $A \models F$ then $A \models G$. We say $G$ is a **consequence** of $F$.
+- $F \equiv G$ iff $F \models G$ and $G \models F$. We say $F$ and $G$ are **equivalent**.
+- Let $\Gamma = {F_1, F_2, F_3,...}$ be a set of formulas.
+	- $A \models \Gamma$ iff $A \models F_i$ for each formula $F_i$ in $\Gamma$. We say $A$ models $\Gamma$.
+	- $\Gamma \models G$ iff $A \models \Gamma$ implies $A \models G$ for every assignment $A$. We say $G$ is a **consequence** of $\Gamma$.
+
+   > [!tip]+ Proposition
+   >  - $F \models G$ iff $\models F \implies G$.
+   >  - $\Gamma \models G$ and $\Gamma$ finite iff $\models \land \Gamma \implies G$.
+   >  
+
+
+### 1.3 Basic Equivalences 
+1. $\neg \neg A \equiv A$
+2. $A \lor A \equiv A$
+3. $A \land A \equiv A$
+4. $A \land \neg A \equiv \bot$
+5. $A \lor \neg A \equiv \top$
+6. $A \lor B \equiv B \lor A$
+7. $A \land B \equiv B \land A$
+8. $A \land \top \equiv A$
+9. $A \lor \top \equiv \top$
+10. $A \land \bot \equiv \bot$
+11. $A \lor \bot \equiv A$
+12. $A \land (B \lor A) \equiv A$
+13. $A \land (B \lor C) \equiv (A \land B) \lor (A \land C)$
+14. $A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)$
+15. $\neg (A \lor B) \equiv \neg A \land \neg B$
+16. $\neg (A \land B) \equiv \neg A \lor \neg B$
+17. $A \implies B \equiv \neg A \lor B$
+18. $A \iff B \equiv (A \implies B) \land (B \implies A)$
+