arXiv:2504.19320v1 宣布类型: 新 摘要: 本文旨在将范畴逻辑应用于设计能够对结构更为丰富的对象进行符号推理的人工智能代理。利用约翰斯顿的带有上下文的形式和术语的 sequent calculus，我们开发了适用于笛卡尔范畴中对象推理的 Horn 逻辑规则的前向链式推理和规范形式算法。我们还将一阶统一化进行改编，以支持多类型理论、上下文和一阶逻辑的片段。这些重新表述的重要性在于，它们可以应用于那些不支持经典逻辑甚至其全部联结词的语义范畴中的对象推理。