Abstract
A propositional logic program P may be identiﬁed with a PfPfcoalgebra on the set of atomic propositions in the program. The corresponding C(PfPf)coalgebra, where C(PfPf) is the cofree comonad on PfPf, describes derivations by resolution. That correspondence has been developed to model ﬁrstorder programs in two ways, with lax semantics and saturated semantics, based on locally ordered categories and right Kan extensions respectively. We unify the two approaches, exhibiting them as complementary rather than competing, reﬂecting the theoremproving and proofsearch aspects of logic programming. While maintaining that unity, we further reﬁne lax semantics to give ﬁnitary models of logic programs with existential variables, and to develop a precise semantic relationship between variables in logic programming and worlds in local state.
Original language  English 

Pages (fromto)  121 
Number of pages  21 
Journal  Journal of Logical and Algebraic Methods in Programming 
Volume  101 
Early online date  19 Jul 2018 
DOIs  
Publication status  Published  Dec 2018 
Keywords
 Logic programming
 Coalgebra
 Coinductive Derivation Tree
 Lawvere theories
 Lax transformations
 Saturation
Fingerprint Dive into the research topics of 'Logic programming: Laxness and Saturation'. Together they form a unique fingerprint.
Profiles

Ekaterina Komendantskaya
 School of Mathematical & Computer Sciences  Professor
 School of Mathematical & Computer Sciences, Computer Science  Professor
Person: Academic (Research & Teaching)