# John Power – Category theoretic semantics for theorem proving in logic programming: embracing the laxness (16 August, 2017)

## by Rob Stewart • September 8, 2017 • DSG Research Seminars: Logic and Programming Languages

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. That correspondence has been developed to model first-order programs in two ways, with lax semantics and saturated semantics, based...

Read more →