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引擎的实现提供了基础。