We discuss the syntax and semantics of relational Horn logic (RHL) and partial Horn logic (PHL). RHL is an extension of the Datalog programming language that allows introducing and equating variables in conclusions. PHL is a syntactic extension of RHL by partial functions and one of the many equivalent notions of essentially algebraic theory. Our main contribution is a new construction of free models. We associate to RHL and PHL sequents classifying morphisms, which enable us to characterize logical satisfaction using lifting properties. We then obtain free and weakly free models using the small object argument. The small object argument can be understood as an abstract generalization of Datalog evaluation. It underpins the implementation of the Eqlog Datalog engine, which computes free models of PHL theories.

翻译：我们讨论了关系Horn逻辑（RHL）和偏Horn逻辑（PHL）的语法与语义。RHL是Datalog编程语言的扩展，允许在结论中引入和等化变量。PHL是通过偏函数对RHL的语法扩展，并且是本质代数理论众多等价表述之一。我们的主要贡献在于提出了一种自由模型的新构造方法。我们为RHL和PHL的相继式关联了分类态射，从而能够利用提升性质来刻画逻辑满足关系。随后，我们通过小对象论证获得了自由模型与弱自由模型。小对象论证可被理解为Datalog求值过程的抽象推广，它为计算PHL理论自由模型的Eqlog Datalog引擎的实现提供了理论基础。