An Evaluation Algorithm for Datalog with Equality
Martin E. Bidlingmaier

TL;DR
This paper introduces an efficient evaluation algorithm for relational Horn logic (RHL), an extension of Datalog that includes equality reasoning, enabling advanced applications like points-to analysis and type inference.
Contribution
It presents a novel evaluation algorithm for RHL that integrates congruence closure techniques, expanding Datalog's capabilities for equality reasoning and complex analysis tasks.
Findings
Incorporates congruence closure into Datalog evaluation for efficiency.
Enables implementation of points-to analysis and type inference using RHL.
Forms the foundation of the Eqlog Datalog engine.
Abstract
We describe an evaluation algorithm for relational Horn logic (RHL). RHL extends Datalog with quantification over sorts, existential quantification in conclusions and, crucially, the ability to infer equalities. These capabilities allow RHL evaluation to subsume and expand applications of Datalog and congruence closure algorithms. We explain how aspects of a fast congruence closure algorithm can be incorporated into Datalog evaluation to obtain an efficient RHL evaluation algorithm. We then sketch how Steensgaard's points-to analysis and type inference can be implemented using RHL evaluation. RHL and the evaluation algorithm described here are the foundation of the Eqlog Datalog engine.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSemantic Web and Ontologies · Advanced Database Systems and Queries · Logic, Reasoning, and Knowledge
