<p>In 1993 paper <a href="https://doi.org/10.1016/0743-1066(93)90040-N" rel="nofollow noreferrer">Equivalence of datalog queries is undecidable</a> Oded Shmueli showed it is in general impossible:</p>

<pre><code>It is shown that determining containment or equivalence of Datalog queries is
recursively unsolvable. 
</code></pre>

<p>The reason for this result is that rules may be 'recursive' (aka 'non-tight'):</p>

<pre><code>ancestor(X, Z) :- ancestor(X, Y), parent(Y, Z)
</code></pre>

<p>and recursion makes the problem undecidable.</p>

<p>It may, however, be possible for fragments of datalog, see <a href="https://arxiv.org/pdf/1406.7801.pdf" rel="nofollow noreferrer">Query Containment for Highly Expressive Datalog Fragments</a></p>
Datalog program containment
<p>given two Datalog programs <code>P1, P2</code> I would like to check if <code>P1</code> is contained in <code>P2</code>, i.e. on every Database <code>D</code>, the ouput of <code>P1</code> is contained in <code>P2</code>.</p>

<p>For example, <code>P1</code>:</p>

<pre><code>A(X,Y) :- a(X,Y)
</code></pre>

<p>and program <code>P2</code>:</p>

<pre><code>A'(X,Y) :- a(X,Y), b(X,Y)
</code></pre>

<p>it is clear that for every possible Database <code>A' contained in A</code>, because <code>b(X,Y)</code> only filters results from <code>a(X,Y)</code> thus the containment.</p>

<p>Is there a standard Datalog implementation that returns true/false on this kind of query?</p>