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求值的抽象推广，它为Eqlog Datalog引擎（用于计算PHL理论的自由模型）的实现提供了理论基础。