[Documentation] Spell check

Author: johanneskloos

doc/architectural/background-concepts.md

@@ -782,7 +782,7 @@ as a vector of 64 propositional variables, say `fac`<sub>0</sub> to
 `fac`<sub>63</sub>, where
 `fac` = 2<sup>63</sup> `fac`<sub>63</sub> + ... + 2<sup>0</sup> `fac`<sub>0</sub>.
 We can then assert that `fac`=1 using
-the propsitional formula
+the propositional formula
 `fac`<sub>63</sub> = 0 and ... and `fac`<sub>1</sub> = 0 and `fac`<sub>0</sub> = 1,
 where we define the formula A = B as ''(A and B) or ((not A) and (not B))''.
 
@@ -855,7 +855,7 @@ abbreviation for a moderately complex formula on bit vectors!
 From the semantics of the `return` instruction, we know that this program will
 return the value `a+b`, so we can describe its behavior as return = A+B.
 
-Let us consider a slighly more complex program.
+Let us consider a slightly more complex program.
 ```C
 int calculate(int x)
 {
@@ -991,7 +991,7 @@ their behavior using a finite propositional formula in the way we have
 done above.
 
 There are multiple approaches to deal with this problem, all with different
-trade-offs. CPROVER chooeses bounded model checking as the underlying approach.
+trade-offs. CPROVER chooses bounded model checking as the underlying approach.
 The idea is that we only consider program
 executions that are, in some measure, ''shorter'' than a given bound. This bound
 then implies an upper bound on the size of the required formulas, which makes