argument to a formal proof

Question

Convert the following argument to a formal proof.

If the software contains a serious bug ($B$), or the hardware is faulty ($H$) then the code will generate an error ($E$). The tests passed ($T$). An error would cause the tests to fail. Therefore the software does not contain a serious bug.

Solution:

$\lnot(B \lor H) \to T$

Is it correct?

Answer 1

No, it is not correct. The argument has $3$ premises ($(B \lor H) \to E$, $T$, $E \to \lnot T$) and one conclusion ($\lnot B$):

$(B \lor H) \to E$

$T$

$E \to \lnot T$

==========

$\lnot B$

The exercise asks to prove that the argument above is valid, i.e. that if you assume the $3$ premises then the conclusion holds by necessity. A formal proof should show, by means of elementary logic steps, how the conclusion follows from the premises. Concretely, the formal proof depends on the inference rules that you are allowed to use.