From 7f8a183b319e3a4a2b3a210f38ad440d52eced2b Mon Sep 17 00:00:00 2001 From: Alice Date: Tue, 19 Sep 2023 12:13:41 +0100 Subject: [PATCH 1/6] vault backup: 2023-09-19 12:13:41 --- .obsidian/workspace.json | 6 +-- Notes/MFES/T - Aula 2 - 18 Setembro 2023.md | 55 +++++++++++++++++++-- 2 files changed, 54 insertions(+), 7 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 3fd318b..e65a886 100644 --- a/.obsidian/workspace.json +++ b/.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", diff --git a/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md b/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md index 5dcd966..45e6ae9 100644 --- a/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md +++ b/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 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)$ + From 4415486b5bfc1f603d520633108ef51198aac3b8 Mon Sep 17 00:00:00 2001 From: Alice Date: Tue, 19 Sep 2023 12:50:29 +0100 Subject: [PATCH 2/6] vault backup: 2023-09-19 12:50:29 --- Notes/MFES/T - Aula 2 - 18 Setembro 2023.md | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md b/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md index 45e6ae9..b26b941 100644 --- a/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md +++ b/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md @@ -58,7 +58,7 @@ A formula $F$ is: - $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. +- 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$. @@ -67,8 +67,18 @@ A formula $F$ is: > - $\Gamma \models G$ and $\Gamma$ finite iff $\models \land \Gamma \implies G$. > + - Let $\Gamma = { F_1, F_2, F_3,... }$ be a set of formulas. + - $\Gamma$ is *consistent* or *satisfiable* iff there is an assignment that models $\Gamma$. + - We say that $\Gamma$ is inconsistent or unsatisfiable iff there is not consistent and denote this by $\Gamma \models \bot$. -### 1.3 Basic Equivalences + > [!tip]+ Proposition + > - {$F, \neg F$} \$models \bot$ + > - If $\Gamma \models \bot$ and $\Gamma \subseteq \Gamma '$, then $\Gamma ' \models \bot$ + > - $\Gamma \models F$ iff $\Gamma, \neg F \models \bot$ + +- Formula + +### 1.2.1 Basic Equivalences 1. $\neg \neg A \equiv A$ 2. $A \lor A \equiv A$ 3. $A \land A \equiv A$ @@ -89,3 +99,5 @@ A formula $F$ is: 18. $A \iff B \equiv (A \implies B) \land (B \implies A)$ + + From 6a435c945d33ce0b397729a02297e3f9f084ac3f Mon Sep 17 00:00:00 2001 From: Alice Date: Tue, 19 Sep 2023 13:08:23 +0100 Subject: [PATCH 3/6] vault backup: 2023-09-19 13:08:23 --- Notes/MFES/T - Aula 2 - 18 Setembro 2023.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md b/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md index b26b941..c857c7a 100644 --- a/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md +++ b/Notes/MFES/T - Aula 2 - 18 Setembro 2023.md @@ -67,16 +67,16 @@ A formula $F$ is: > - $\Gamma \models G$ and $\Gamma$ finite iff $\models \land \Gamma \implies G$. > - - Let $\Gamma = { F_1, F_2, F_3,... }$ be a set of formulas. - $\Gamma$ is *consistent* or *satisfiable* iff there is an assignment that models $\Gamma$. - We say that $\Gamma$ is inconsistent or unsatisfiable iff there is not consistent and denote this by $\Gamma \models \bot$. > [!tip]+ Proposition - > - {$F, \neg F$} \$models \bot$ + > - {$F, \neg F$} $\models \bot$ > - If $\Gamma \models \bot$ and $\Gamma \subseteq \Gamma '$, then $\Gamma ' \models \bot$ > - $\Gamma \models F$ iff $\Gamma, \neg F \models \bot$ -- Formula +- Formula $G$ is a subformula of formula F if it occurs syntactically within F +- Formula G is a strict subformula of F if G is a subformula of $F$ and $G \neg \equals F$ ### 1.2.1 Basic Equivalences 1. $\neg \neg A \equiv A$ From a7847219ff9fffe603081093daf4d2145f32e7df Mon Sep 17 00:00:00 2001 From: Alice Date: Tue, 19 Sep 2023 13:15:39 +0100 Subject: [PATCH 4/6] vault backup: 2023-09-19 13:15:39 --- .obsidian/workspace.json | 30 ++++++++++++++++++++-------- Notes/CP/T - Aula 2 - 19 Setembro.md | 3 +++ 2 files changed, 25 insertions(+), 8 deletions(-) create mode 100644 Notes/CP/T - Aula 2 - 19 Setembro.md diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index e65a886..116b188 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -18,8 +18,21 @@ "source": false } } + }, + { + "id": "33ee032389b5d04b", + "type": "leaf", + "state": { + "type": "markdown", + "state": { + "file": "Notes/CP/T - Aula 2 - 19 Setembro.md", + "mode": "source", + "source": false + } + } } - ] + ], + "currentTab": 1 } ], "direction": "vertical" @@ -69,8 +82,7 @@ } ], "direction": "horizontal", - "width": 300, - "collapsed": true + "width": 300 }, "right": { "id": "fe57fca15d81c25f", @@ -86,7 +98,7 @@ "state": { "type": "backlink", "state": { - "file": "Notes/MFES/T - Aula 2 - 18 Setembro 2023.md", + "file": "Notes/CP/T - Aula 2 - 19 Setembro.md", "collapseAll": false, "extraContext": false, "sortOrder": "alphabetical", @@ -103,7 +115,7 @@ "state": { "type": "outgoing-link", "state": { - "file": "Notes/MFES/T - Aula 2 - 18 Setembro 2023.md", + "file": "Notes/CP/T - Aula 2 - 19 Setembro.md", "linksCollapsed": false, "unlinkedCollapsed": true } @@ -126,7 +138,7 @@ "state": { "type": "outline", "state": { - "file": "Notes/MFES/T - Aula 2 - 18 Setembro 2023.md" + "file": "Notes/CP/T - Aula 2 - 19 Setembro.md" } } } @@ -150,10 +162,12 @@ "obsidian-excalidraw-plugin:Create new drawing": false } }, - "active": "201fe1705c33e116", + "active": "33ee032389b5d04b", "lastOpenFiles": [ - "README.md", "Notes/MFES/T - Aula 2 - 18 Setembro 2023.md", + "Notes/CP/T - Aula 2 - 19 Setembro.md", + "Notes/CP", + "README.md", "Notes/MFES/MFES - UC Details.md", "2023-09-18.md", "MFES/T - Aula 2 - 18 Setembro 2023.md", diff --git a/Notes/CP/T - Aula 2 - 19 Setembro.md b/Notes/CP/T - Aula 2 - 19 Setembro.md new file mode 100644 index 0000000..edc4bf3 --- /dev/null +++ b/Notes/CP/T - Aula 2 - 19 Setembro.md @@ -0,0 +1,3 @@ +## Conteúdo +- cache em arquiteturas multicore +- \ No newline at end of file From 2e6ee5cbf42556b0bb883045c20fc9e5c5514916 Mon Sep 17 00:00:00 2001 From: Alice Date: Tue, 19 Sep 2023 13:24:03 +0100 Subject: [PATCH 5/6] vault backup: 2023-09-19 13:24:03 --- Notes/CP/T - Aula 2 - 19 Setembro.md | 1 + 1 file changed, 1 insertion(+) diff --git a/Notes/CP/T - Aula 2 - 19 Setembro.md b/Notes/CP/T - Aula 2 - 19 Setembro.md index edc4bf3..2f8b8a0 100644 --- a/Notes/CP/T - Aula 2 - 19 Setembro.md +++ b/Notes/CP/T - Aula 2 - 19 Setembro.md @@ -1,3 +1,4 @@ ## Conteúdo - cache em arquiteturas multicore +- code profiling - \ No newline at end of file From 8e825970686292bd5a28d188d09ec67e637108dd Mon Sep 17 00:00:00 2001 From: Alice Date: Tue, 19 Sep 2023 13:39:51 +0100 Subject: [PATCH 6/6] vault backup: 2023-09-19 13:39:51 --- Notes/CP/T - Aula 2 - 19 Setembro.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Notes/CP/T - Aula 2 - 19 Setembro.md b/Notes/CP/T - Aula 2 - 19 Setembro.md index 2f8b8a0..307e4e0 100644 --- a/Notes/CP/T - Aula 2 - 19 Setembro.md +++ b/Notes/CP/T - Aula 2 - 19 Setembro.md @@ -1,4 +1,7 @@ ## Conteúdo - cache em arquiteturas multicore - code profiling +- instruction-level paralelism +- Data dependency +- branch prediction - \ No newline at end of file