Merge branch 'main' of ssh://git.olympuslab.net:522/Alice/The_Sauce_Notes
This commit is contained in:
commit
167e399365
SSH key fingerprint:
SHA256:JiuxZNdA5bRWXPMUJChI0AQ75yC+cXY4xM0IaVwEVys
3 changed files with 93 additions and 13 deletions
32
.obsidian/workspace.json
vendored
32
.obsidian/workspace.json
vendored
|
|
@ -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,15 +162,17 @@
|
|||
"obsidian-excalidraw-plugin:Create new drawing": false
|
||||
}
|
||||
},
|
||||
"active": "4c008c59a631fa8d",
|
||||
"active": "33ee032389b5d04b",
|
||||
"lastOpenFiles": [
|
||||
"Notes/MFES/MFES - UC Details.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",
|
||||
"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",
|
||||
|
|
|
|||
7
Notes/CP/T - Aula 2 - 19 Setembro.md
Normal file
7
Notes/CP/T - Aula 2 - 19 Setembro.md
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
## Conteúdo
|
||||
- cache em arquiteturas multicore
|
||||
- code profiling
|
||||
- instruction-level paralelism
|
||||
- Data dependency
|
||||
- branch prediction
|
||||
-
|
||||
|
|
@ -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,57 @@ 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$.
|
||||
>
|
||||
|
||||
- $\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$
|
||||
> - If $\Gamma \models \bot$ and $\Gamma \subseteq \Gamma '$, then $\Gamma ' \models \bot$
|
||||
> - $\Gamma \models F$ iff $\Gamma, \neg F \models \bot$
|
||||
|
||||
- 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$
|
||||
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)$
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue