反拟阵的 Horn 规则表示及其在教育系统中的应用

受反拟阵近期在计算机辅助教育系统中应用的启发，我们研究了反拟阵的 Horn 规则表示。我们将任意 Horn 规则集 $\mathcal{R}$ 与唯一的极大反拟阵 $\mathcal{A}(\mathcal{R})$ 相关联，该反拟阵包含在由 $\mathcal{R}$ 自然确定的并闭族 $\mathcal{K}(\mathcal{R})$ 中。我们探讨了将 $\mathcal{R}$ 视为输入时关联 $\mathcal{R} \mapsto \mathcal{A}(\mathcal{R})$ 的算法和布尔函数理论方面的问题。我们提出了线性时间算法来解决 $\mathcal{A}(\mathcal{R})$ 的成员资格问题和推理问题。我们还提供了生成 $\mathcal{A}(\mathcal{R})$ 的所有成员和所有蕴涵项的高效算法。我们证明了这种表示本质上等价于反拟阵的 Korte-Lovász 有根集表示。基于这种等价性，我们提供了一个二次时间算法来构造唯一确定的最小表示。这些结果对计算机辅助教育系统具有潜在的应用价值，其中反拟阵被用作学习者可能知识状态空间的模型，并通过向人类专家提出 Horn 查询来构建。