maybe one or the other here is familiar with model-based diagnostics, or perhaps with mathematical logic.
I have a question that probably refers more to the logic behind it. I'll start to explain the problem. Given is a Inverter, if the input of the inverter is 0, then the output is 1 and vice versa. This is always the case if and only if the inverter works correctly.
Now there is a system description called SD, some components COMPs and once the case that the inverter is faulty and once, the case where the inverter works properly, and some observations OBS
Here are a few definitions:
$Ab(c)$: component c is ABnormal
$\lnot Ab(c)$: component c is not abnormal, i.e. normal
Inverter: $X$
A drawing of the inverter:
For example, a (presumed) system description of the inverter might look like this: $$SD = \{\{A \land \lnot Ab(X) \rightarrow \lnot C\}, \{\lnot A \land \lnot Ab(X) \rightarrow C\}\}$$ Then there is, for example, the Observations OBS abbreviated: $$OBS = \{A=1,C=1\}$$ That would mean with the input 1 resulted the 1, at the first sight considered something seems not to function properly in the circuit.
I'm trying to understand exactly this: $$SD \cup \{A=1,C=1\}\cup\{\lnot Ab(X)\}\models\bot \quad\quad Eq.1$$ and this: $$SD \cup \{A=1,C=1\}\cup\{Ab(X)\}\not\models\bot \quad\quad Eq.2$$
I would just demonstrate what I am thinking at the moment about Equation Eq.2: I do not know if that's right: $$\{\{A \land \lnot Ab(X) \rightarrow \lnot C\}, \{\lnot A \land \lnot Ab(X) \rightarrow C\}\} \cup \{A=1,C=1\}\cup\{Ab(X)\}\not\models\bot $$ I transform the logical implications once: $$\{\{\lnot A \lor Ab(X) \lor \lnot C\}, \{A \lor \lnot Ab(X) \lor C\}\} \cup \{A=1,C=1\}\cup\{Ab(X)\}\not\models\bot $$ To judge by equation Eq.2 this would have to mean: Assumption X is abnormal is consistent. If I understand Eq.2 correctly. Then Eq.1 would have to mean: assumption X is normal is inconsistent, right?
My question is, how exactly do you do this set-up $SD \cup ... \cup$? How could you get from: $$\{\{A \land \lnot Ab(X) \rightarrow \lnot C\}, \{\lnot A \land \lnot Ab(X) \rightarrow C\}\} \cup \{A=1,C=1\}\cup\{Ab(X)\}$$ to conclude the consistency / inconsistency, what should be done?
I hope it's reasonably clear what I mean. Thank you for coming answers!