# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Propositional Logic
#### 2.4.2 Semantics of Propositional Logic
: _Given a set of propositional variables \(AP\), a propositional formula \(F\) over \(\text{Vars}(F)\) and a truth assignment \(\mu\) over \(A\subseteq AP\) with \(\text{Vars}(F)\subseteq A\)we give the following inductive definition of when \(\mu\)_ satisfies \(F\) (_or equivalently, \(F\) evaluates to \(\top\) under \(\mu\)_), denoted as \(\mu\models F\):_  
* \(\mu\models\top\) _and_ \(\mu\
ot\models\bot\)_._
* _For each_ \(a\in\operatorname{Vars}(F)\)_,_ \(\mu\models a\) _iff_ \(\mu(a)=\top\)_._
* \(\mu\models\
eg F\) _iff_ \(\mu\
ot\models F\)_._
* \(\mu\models F_{1}\wedge F_{2}\) _iff_ \(\mu\models F_{1}\) _and_ \(\mu\models F_{2}\)_._
* \(\mu\models F_{1}\lor F_{2}\) _iff_ \(\mu\models F_{1}\) _or_ \(\mu\models F_{2}\)_._  
The semantics of other logical connectives can easily be inferred from their truth tables. We provide the following useful definitions:  
**Definition 15** ((Propositional) Models). : _Given a propositional formula \(F\), a truth assignment \(\mu:\operatorname{Vars}(F)\to\mathbb{B}\) is a model (or satisfying assignment) of \(F\) iff \(\mu\models F\)._  
**Definition 16** ((Propositional or Boolean) Satisfiability). : _A propositional formula \(F\) is said to be satisfiable iff it has at least one model, i.e., there exists \(\mu\) such that \(\mu\models F\). Otherwise, \(F\) is said to be unsatisfiable._  
**Definition 17** ((Propositional) Consequence). : _Given a set of propositional formulas \(\Phi\) and a propositional formula \(F\) such that \(\operatorname{Vars}(F)\subseteq\operatorname{Vars}(\Phi)\), \(F\) is said to be a consequence of \(\Phi\) iff every model of \(\Phi\) can be restricted to a model for \(F\), denoted as \(\Phi\models F\)._  
**Definition 18** ((Propositional) Equivalence). : _Given two propositional formulas \(F\) and \(G\) such that \(\operatorname{Vars}(F)=\operatorname{Vars}(G)\), \(F\) is said to be equivalent to \(G\) iff every model of \(F\) is also a model of \(G\) and vice versa, denoted as \(F\equiv G\)._  
**Definition 19** ((Propositional) Validity). : _An argument from a set of propositional formulas \(\Phi\) to a conclusion \(F\) is valid iff \(\Phi\models F\)._  
**Definition 20** ((Propositional) Consistency). : _A set of propositional formulas \(\Phi\) is consistent iff there is a complete truth assignment \(\mu\) that is a model for every formula of \(\Phi\)._  
**Definition 21** (Valid Propositional Formulas). : _A propositional formula \(F\) is said to be a valid (or a tautology), denoted as \(\models F\), iff every truth assignment over its variables is a model for it._  
**Definition 22** (Strength of Propositional Formulas). : _Given two propositional formulas \(F\) and \(G\), if \(F\models G\) then \(F\) is said to be stronger than \(G\) and, conversely, \(G\) is said to be weaker than \(F\). From the semantics of implication (\(\rightarrow\)), it is clear that, if \(\models F\to G\), then \(F\models G\) and, thus, \(F\) is stronger than \(G\)._  
We also provide the following remarks about notation for models and truth assignment. **Notation 1** (Formulas as Set of Models). : _Given a propositional formula \(F\), we denote with \(\operatorname{Mods}(F)\) the set of all models of \(F\). Any propositional formula \(F\) can be seen as a representation of its set of models \(\operatorname{Mods}(F)\)._  
Any truth assignment can be represented as a formula satisfied by it or the set of propositional variables it assigns to \(\top\). **Notation 2** (Restriction of Models). : _Given a propositional formula \(F\), a truth assignment \(\mu:A\to\mathbb{B}\), with \(\operatorname{Vars}(F)\subset A\) can be restricted to a model of \(F\) iff its restriction \(\mu\big{|}_{\operatorname{Vars}(F)}\models F\)._  
**Notation 3** (Truth Assignments as Formulas). : _A truth assignment \(\mu\) over a set of propositional variables \(A\in AP\) can be represented as the following propositional formula:_  
\[F_{\mu}\stackrel{{\text{\tiny{def}}}}{{=}}\bigwedge_{a_{i}\in A}l_{i }\text{ where }