Modus Tollens（MT）是经典的推理规则，反事实是与事实相反的假设性陈述，反事实推理则是基于此类陈述的推理过程。否定在上述概念中居于核心位置。本文基于逻辑系统 LCOI 与 PLCOI，引入三种否定：矛盾否定、相反否定和中介否定，分别构造三种 Modus Tollens 变体，记为 MTC、MTO、MTI。我们在每个系统中给出蕴含的形式化定义，并给出对应的真值计算算法，例如在 MTC 中，若前提 $P$ 为真，则结论 $Q$ 的真值等于第二前提 $\neg_{c} P$ 的真值，其中 $\neg_{c}$ 表示矛盾否定。随后讨论这些算法的可约性。为了将三种否定引入反事实及其推理，本文将反事实分为是否含有逻辑否定的两类，进而提出基于矛盾、相反和中介否定的三种反事实及其推理形式。我们证明，这三种反事实推理的推理形式分别与 MTC、MTO、MTI 完全一致，即它们共享相同的推理结构。因而 MTC、MTO、MTI 的真值算法同样适用于对应的反事实推理。算法表明：若推理的第一前提为真，则结论的真值与对应的负前提的真值相同，体现了算法的一致性与准确性。
点评