Logic-Based Artificial Intelligence Algorithms Supporting Categorical Semantics
This work addresses the challenge of reasoning in semantic categories that lack classical logic support, which is incremental as it builds on existing categorical logic frameworks.
The paper tackled the problem of designing AI agents for symbolic reasoning about objects in non-classical semantic categories by applying categorical logic, resulting in forward chaining and normal form algorithms adapted for cartesian categories with Horn logic and multi-sorted unification.
This paper seeks to apply categorical logic to the design of artificial intelligent agents that reason symbolically about objects more richly structured than sets. Using Johnstone's sequent calculus of terms- and formulae-in-context, we develop forward chaining and normal form algorithms for reasoning about objects in cartesian categories with the rules for Horn logic. We also adapt first-order unification to support multi-sorted theories, contexts, and fragments of first-order logic. The significance of these reformulations rests in the fact that they can be applied to reasoning about objects in semantic categories that do not support classical logic or even all its connectives.