Datalog with First-Class Facts

TL;DR

The paper introduces DL$^{orall!}$, a novel Datalog extension with first-class facts using unique Skolem terms, enabling efficient reasoning over tree-structured data and outperforming existing systems in scalability.

Contribution

It proposes DL$^{orall!}$, a new Datalog variant with first-class facts, and implements it in Slog, demonstrating improved scalability and performance over existing systems.

Findings

Slog outperforms Nemo, Vlog, RDFox, and Soufflé on benchmarks.

DL$^{orall!}$ enables reasoning over tree-structured data efficiently.

System scales to thousands of threads in parallel execution.

Abstract

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.