Date: Mon, 22 Jan 1996 23:42:51 -0500 From: James Otto <otto@triples.math.mcgill.ca> Dear People, The plain text draft paper, whose title and abstract follows, is availabe by web or ftp at ftp://triples.math.mcgill.ca/pub/otto/res and is linked to ftp://triples.math.mcgill.ca/pub/otto/otto.html Best regards, Jim From Horn formula to Makkai sketch resolution J. Otto January 22, 1996 otto@triples.math.mcgill.ca Abstract. We provide a basis for logic programming into locally finitely presentable (or l.f.p.) categories. We thus begin to consider higher order logic programming. Horn formulas, in particular systems of equations, generalize to finite Makkai (or M-) sketches. Further, models of sets of Horn clauses generalize to, again called models and forming the l.f.p. categories, M-sketches orthogonal to sets of maps (axioms) between finite M-sketches. Resolutions compute maps (answers) from finite M-sketches (queries) to initial models. Resolutions are cospans and lift to compositions of special resolutions.