Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Logic-Based Artificial Intelligence Algorithms Supporting Categorical Semantics

Ralph Wojtowicz

TL;DR

The paper presents a framework for logic-based AI grounded in categorical semantics, reframing inference and unification for multi-sorted, context-rich theories within cartesian and related categories. It adapts Johnstone's sequent calculus (Elephant) to forward-chaining and normal-form Horn theories, deriving both propositional and first-order Horn inference algorithms that respect terms- and formulae-in-context. Central contributions include algorithms for Horn normalization, context-aware unification, and first-order Horn forward chaining, supported by a rigorous semantic justification via Sigma-Structures and pullback/subobject semantics. By enabling reasoning in semantic categories that do not support full classical logic, the work broadens the applicability of symbolic AI to richer mathematical structures and dynamic interpretations, with a practical realization path via C implementations and connections to established theorem provers. Overall, it provides a principled bridge between categorical logic and AI inference, offering concrete methods and proofs to perform sound symbolic reasoning in non-classical semantic settings.

Abstract

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.

Logic-Based Artificial Intelligence Algorithms Supporting Categorical Semantics

TL;DR

The paper presents a framework for logic-based AI grounded in categorical semantics, reframing inference and unification for multi-sorted, context-rich theories within cartesian and related categories. It adapts Johnstone's sequent calculus (Elephant) to forward-chaining and normal-form Horn theories, deriving both propositional and first-order Horn inference algorithms that respect terms- and formulae-in-context. Central contributions include algorithms for Horn normalization, context-aware unification, and first-order Horn forward chaining, supported by a rigorous semantic justification via Sigma-Structures and pullback/subobject semantics. By enabling reasoning in semantic categories that do not support full classical logic, the work broadens the applicability of symbolic AI to richer mathematical structures and dynamic interpretations, with a practical realization path via C implementations and connections to established theorem provers. Overall, it provides a principled bridge between categorical logic and AI inference, offering concrete methods and proofs to perform sound symbolic reasoning in non-classical semantic settings.

Abstract

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.
Paper Structure (47 sections, 50 theorems, 10 equations, 3 figures, 16 algorithms)

This paper contains 47 sections, 50 theorems, 10 equations, 3 figures, 16 algorithms.

Table of Contents

  1. Introduction
  2. Categorical Logic
  3. Syntax
  4. Terms and Formulae
  5. Substitution
  6. Deduction
  7. Sequents vs Formulae
  8. Horn Clauses vs Horn Sequents
  9. Normal Form for Horn Theories
  10. Semantics
  11. $\Sigma$-Structures
  12. Terms- and Formulae-in Context
  13. Substitution
  14. Forward Chaining for Propositional Horn Theories
  15. Unification of Terms- and Formulae-in Context
  16. ...and 32 more sections

Key Result

Lemma 2.1

Lemma: Let $\vec{z}.\,e_1$ and $\vec{z}.\,e_2$ be expressions-in-context with the same context and let $\theta=[\vec{s}/\vec{y}\,]$ be a substitution. Then $(\vec{z}.\,e_1)\,\theta$ and $(\vec{z}.\,e_2)\,\theta$ have the same context.

Theorems & Definitions (50)

  • Lemma 2.1
  • Theorem 2.2
  • Theorem 2.3
  • Theorem 2.4
  • Theorem 2.5
  • Theorem 2.6
  • Theorem 4.1
  • Lemma 4.2
  • Lemma 4.3
  • Theorem 4.4
  • ...and 40 more