Horn非子句类及其多项式时间可判定性

命题非子句（NC）公式的表达能力比子句公式丰富指数级。然而，子句效率优于非子句效率。事实上，后者的一大弱点是：尽管Horn子句公式与Horn算法对子句推理的高效率至关重要，但此前未提出过非子句形式的类Horn公式。为克服此弱点，我们通过将Horn模式适当提升为NC形式，定义了Horn非子句（Horn-NC）公式的混合类$\mathbb{H_{NC}}$，并主张$\mathbb{H_{NC}}$及未来的Horn-NC算法将如Horn类提升子句效率一般提升非子句效率。其次，我们：（i）给出$\mathbb{H_{NC}}$的紧凑归纳定义；（ii）证明在语法上$\mathbb{H_{NC}}$包含Horn类，但语义上两类等价；（iii）刻画属于$\mathbb{H_{NC}}$的非子句公式。第三，我们定义非子句单元归结演算$UR_{NC}$，并证明其在多项式时间内判定$\mathbb{H_{NC}}$的可满足性。据我们所知，这一事实使$\mathbb{H_{NC}}$成为NC推理中首个被刻画的多项式类。最后，我们证明$\mathbb{H_{NC}}$可线性识别，且比Horn类严格更简洁并丰富指数级。我们讨论在NC自动推理（如可满足性求解、定理证明、逻辑编程等）中可直接受益于$\mathbb{H_{NC}}$与$UR_{NC}$，并且作为其已证性质的副产品，$\mathbb{H_{NC}}$成为分析Horn函数与蕴涵系统的新替代方案。