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

2016/02/17 by Komendantskaya, Ekaterina, Power, John
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1602.05400

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.

Related

• Logic programming: laxness and saturation
• A Survey of the Proof-Theoretic Foundations of Logic Programming
• A uniform approach to logic programming semantics
• Logic Without Syntax
• A Well-Founded Semantics for FOL-Programs