Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/HarvardPL/AbcDatalog/llms.txt

Use this file to discover all available pages before exploring further.

DatalogEngineWithProvenance extends DatalogEngine with support for why-provenance queries. After initializing and querying the engine as usual, you can call getJustification to retrieve the last rule that was used to derive a specific ground fact. By recursively calling getJustification on the body atoms of the returned clause, you can reconstruct a full provenance tree explaining why any derived fact holds. All methods from DatalogEngine — init, query(PositiveAtom), and query(List<PositiveAtom>) — are available unchanged. See the DatalogEngine reference for their documentation.

​
Methods

​
getJustification

Clause getJustification(PositiveAtom fact)
Returns the last clause (rule instance) used to derive the given ground fact. The returned clause is fully ground (variable-free): both the head and every body atom contain only constants. Returns null if the atom is an EDB base fact (not derived by any rule) or has not been derived at all.
​
fact
PositiveAtom
required
A ground atom (all arguments must be constants) whose provenance you want to inspect.
​
result
Clause
A ground, variable-free clause whose head matches fact. The body lists the ground premises used to fire the rule. Returns null if the fact is not derived.
To build a complete provenance tree, iterate over the body of the returned clause and call getJustification on each PositiveAtom premise recursively. When getJustification returns null for a body atom, that atom is a base EDB fact — the leaf of the derivation tree.

​
Code example

The following example is adapted from SemiNaiveEngine.main: 
import edu.harvard.seas.pl.abcdatalog.ast.Clause;
import edu.harvard.seas.pl.abcdatalog.ast.PositiveAtom;
import edu.harvard.seas.pl.abcdatalog.ast.Premise;
import edu.harvard.seas.pl.abcdatalog.engine.DatalogEngineWithProvenance;
import edu.harvard.seas.pl.abcdatalog.engine.bottomup.sequential.SemiNaiveEngine;
import edu.harvard.seas.pl.abcdatalog.parser.DatalogParser;
import edu.harvard.seas.pl.abcdatalog.parser.DatalogTokenizer;
import java.io.StringReader;
import java.util.Set;

String src =
    "edge(a,b). edge(b,c). edge(c,d). edge(d,c)."
    + "tc(X,Y) :- edge(X,Y)."
    + "tc(X,Y) :- tc(X,Z), tc(Z,Y).";

DatalogTokenizer t = new DatalogTokenizer(new StringReader(src));
Set<Clause> prog = DatalogParser.parseProgram(t);

DatalogEngineWithProvenance engine = SemiNaiveEngine.newEngineWithProvenance();
engine.init(prog);

// Ask why tc(c,c) holds
DatalogTokenizer qt = new DatalogTokenizer(new StringReader("tc(c,c)?"));
PositiveAtom q = DatalogParser.parseQuery(qt);

Clause lastClause = engine.getJustification(q);
System.out.println(lastClause);  // e.g. tc(c,c) :- tc(c,c), tc(c,c).

for (Premise p : lastClause.getBody()) {
    if (p instanceof PositiveAtom) {
        Clause parent = engine.getJustification((PositiveAtom) p);
        System.out.println(parent);
        for (Premise p2 : parent.getBody()) {
            System.out.println(engine.getJustification((PositiveAtom) p2));
        }
    }
}

​
Concrete implementation

The only current implementation is SemiNaiveEngine, obtained through the factory method: 
DatalogEngineWithProvenance engine = SemiNaiveEngine.newEngineWithProvenance();
To get a plain DatalogEngine without provenance tracking (lower memory overhead), use SemiNaiveEngine.newEngine() instead.

Build docs developers (and LLMs) love

Get started for freeTalk to us