Category theoretic semantics for theorem proving in logic programming: embracing the laxness

TL;DR

This paper develops a category theoretic framework for understanding logic programming semantics, extending it to first-order and arbitrary programs using lax semantics and refining existing saturation semantics.

Contribution

It introduces a novel categorical semantics for logic programming that encompasses first-order and arbitrary programs through lax semantics and refines existing saturation semantics.

Findings

Extended lax semantics to first-order logic programs without existential variables.

Captured proofs by term-matching resolution in logic programming.

Refined saturation semantics to complement lax semantics.

Abstract

A propositional logic program $P$ may be identified with a $P_fP_f$-coalgebra on the set of atomic propositions in the program. The corresponding $C(P_fP_f)$-coalgebra, where $C(P_fP_f)$ is the cofree comonad on $P_fP_f$, describes derivations by resolution. Using lax semantics, that correspondence may be extended to a class of first-order logic programs without existential variables. The resulting extension captures the proofs by term-matching resolution in logic programming. Refining the lax approach, we further extend it to arbitrary logic programs. We also exhibit a refinement of Bonchi and Zanasi's saturation semantics for logic programming that complements lax semantics.