# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Propositional Logic
#### 2.4.2 Semantics of Propositional Logic  
Intuitively, from the semantic point of view, propositional variables represent atomic propositions, logical constants represent special propositions that are either always true (\(\top\)) or always false (\(\bot\)) and logical connectives represent standard Boolean functions such as logical negation (\(\
eg\)), logical conjunction (\(\land\)) and logical disjunction (\(\lor\)). Each propositional variable is interpreted as an atomic proposition about the domain of discourse which can either be true or false. Such an interpretation is described by means of a _truth assignment_ defined as follows. **Definition 12** (Truth Assignments). : _Given a set of propositional variables \(A\subseteq AP\), a truth assignment \(\mu:A\rightarrow\mathbb{B}\) is a function mapping each propositional variable \(a\in A\) to a truth value in \(\mathbb{B}\)._  
Note that, from the model-theoretic perspective, truth assignments can be seen as equivalent representations of structures along with a definition of truth. Since the only non-logical symbols of propositional logic are propositional variables, a structure for the propositional language is an interpretation of those variables as atomic propositions on the domain of discourse. A definition of truth then maps each atomic proposition to a truth value. The composition of the two is equivalent to a truth assignment. **Definition 13** (Complete or Partial Truth Assignments). : _Given a propositional formula \(F\), a complete truth assignment for \(F\) is a function \(\mu:\text{Vars}(F)\rightarrow\mathbb{B}\) assigning a truth value to each variable of \(F\). A partial truth assignment for \(F\) is a function \(\mu:A\subset\text{Vars}(F)\rightarrow\mathbb{B}\) assigning a truth value to a subset \(A\) of the variables of \(F\)._  
Each logical connective is given a _truth-functional interpretation_, mapping it to a specific _Boolean function_. Logical connectives are therefore thought as having a certain _arity_, according to the Boolean function they represent: logical conjunction and disjunction are binary connectives whereas negation is a unary connective. Under its truth-functional interpretation, each logical connective of arity \(n\) corresponds to a Boolean function \(f:\mathbb{B}^{n}\rightarrow\mathbb{B}\) mapping the truth value of its operands to the truth value of its result. The truth-functional interpretation of logical connectives is usually described by means of truth tables. Additional logical connectives, representing other standard Boolean functions such as implication (\(\rightarrow\)), bi-implication (\(\leftrightarrow\)) and exclusive disjunction (\(\oplus\)), may be included in the language of propositional logic according to their usual semantics and and syntactic definition, following. \[F_{1}\to F_{2}\stackrel{{\text{def}}}{{=}}\
eg F_{1} \lor\
eg F_{2} \tag{2}\] \[F_{1}\leftrightarrow F_{2}\stackrel{{\text{def}}}{{= }}(\
eg F_{1}\land\
eg F_{2})\lor(F_{1}\wedge F_{2})\] (3) \[F_{1}\oplus F_{2}\stackrel{{\text{def}}}{{=}}(\
eg F _{1}\wedge F_{2})\lor(F_{1}\land\
eg F_{2}) \tag{4}\]  
As a way of reducing the number of necessary parentheses, the following precedence order between logical operators is usually applied (from highest precedence to lowest precedence): \(\
eg\), \(\land\), \(\lor\), \(\rightarrow\), \(\leftrightarrow\) and \(\oplus\). Each propositional formula, therefore, unambiguously represents a given Boolean function, which can be determined combining the function associated with its logical connectives according to the precedence order. **Definition 14** (Semantics of Propositional Logic).