Subject: draft paper: From Horn formula to Makkai sketch resolution

From: categories <[email-masked]>
Date: Tue, 23 Jan 1996 21:08:29 -0400 (AST)

Date: Mon, 22 Jan 1996 23:42:51 -0500
From: James Otto <[email-masked]>
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

		     [email-masked]

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.