In certain steps, when the De Morgan Theorem is needed to use an inference rule, the program uses the De Morgan Theorem but does not state it explicitly in the deduction steps.
e.g., If the logical expression Q∧P is present, and given the premise P→¬(¬Q∨¬P)), deducing ¬P with Modus Tollens may omit explicitly identifying the intermediary step involving the application of De Morgan's law on Q∧P.
Type: Bug
Reported by User
Description:
In certain steps, when the De Morgan Theorem is needed to use an inference rule, the program uses the De Morgan Theorem but does not state it explicitly in the deduction steps.
e.g., If the logical expression Q∧P is present, and given the premise P→¬(¬Q∨¬P)), deducing ¬P with Modus Tollens may omit explicitly identifying the intermediary step involving the application of De Morgan's law on Q∧P.