2025/04/27 by Ralph L. Wojtowicz, Wojtowicz, Ralph
Computer Science · #03 #18 #Artificial Intelligence (cs.AI) #Constraint Satisfaction and Optimization #FOS: Computer and information sciences #I.1.2 #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2504.19320
openalex publication_date 2025/04/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.