Datalog is a popular logic programming language for deductive reasoning tasks in a wide array of applications, including business analytics, program analysis, and ontological reasoning. However, Datalog's restriction to flat facts over atomic constants leads to challenges in working with tree-structured data, such as derivation trees or abstract syntax trees. To ameliorate Datalog's restrictions, popular extensions of Datalog support features such as existential quantification in rule heads (Datalog$^\pm$, Datalog$^\exists$) or algebraic data types (Souffl\'e). Unfortunately, these are imperfect solutions for reasoning over structured and recursive data types, with general existentials leading to complex implementations requiring unification, and ADTs unable to trigger rule evaluation and failing to support efficient indexing. We present DL$^{\exists!}$, a Datalog with first-class facts, wherein every fact is identified with a Skolem term unique to the fact. We show that this restriction offers an attractive price point for Datalog-based reasoning over tree-shaped data, demonstrating its application to databases, artificial intelligence, and programming languages. We implemented DL$^{\exists!}$ as a system \slog{}, which leverages the uniqueness restriction of DL$^{\exists!}$ to enable a communication-avoiding, massively-parallel implementation built on MPI. We show that Slog outperforms leading systems (Nemo, Vlog, RDFox, and Souffl\'e) on a variety of benchmarks, with the potential to scale to thousands of threads.

翻译：Datalog是一种流行的逻辑编程语言，广泛应用于商业分析、程序分析和本体推理等领域的演绎推理任务。然而，Datalog仅限于基于原子常量的扁平事实，这给处理树形结构数据（如推导树或抽象语法树）带来了挑战。为了改善Datalog的限制，其主流扩展支持诸如规则头中的存在量化（Datalog$^\pm$、Datalog$^\exists$）或代数数据类型（Souffl\'e）等特性。遗憾的是，这些方案对于结构化及递归数据类型的推理并不完善：通用的存在量化导致需要复杂合一运算的实现，而代数数据类型无法触发规则求值且不支持高效索引。本文提出DL$^{\exists!}$，一种具有一等事实的Datalog，其中每个事实都通过一个该事实独有的Skolem项进行标识。我们证明这种限制为基于Datalog的树形数据推理提供了理想的性能平衡点，并展示了其在数据库、人工智能和编程语言领域的应用。我们将DL$^{\exists!$实现为名为\slog{}的系统，该系统利用DL$^{\exists!}$的唯一性限制，构建了基于MPI的免通信大规模并行实现。实验表明，Slog在多种基准测试中优于主流系统（Nemo、Vlog、RDFox和Souffl\'e），并具备扩展到数千线程的潜力。