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.

Beyond positive atoms, AbcDatalog rule bodies can contain three additional kinds of premises: explicit unification (=), explicit disunification (!=), and negated atoms (not). Each of these extends what you can express, but each also carries safety requirements and must be explicitly enabled in DatalogValidator before the engine will accept them.

​
Explicit unification

The = operator, represented by the BinaryUnifier AST node, requires two terms to unify. When both terms are variables, it equates them; when one is a constant, it binds the variable to that constant. 
% Detect nodes that can reach themselves — i.e., nodes in a cycle.
% X=Y constrains the result to pairs where both positions are equal.
in_cycle1(X) :- tc(X,Y), X=Y.

% Equivalent formulation without explicit unification:
in_cycle2(X) :- tc(X,X).
Both rules above derive the same relation. The X=Y form is useful when a variable has already been introduced by a different body atom and you need to assert equality after the fact.
Unification can also bind a variable to a constant: X=a fixes X to the constant a for the rest of the rule. This also satisfies the safety requirement for X — a variable unified with a constant is considered bound.

​
Enabling unification in the validator

Unification in rule bodies is an optional feature. You must opt in via DatalogValidator before calling validate: 
DatalogValidator validator = new DatalogValidator()
    .withBinaryUnificationInRuleBody();

UnstratifiedProgram program = validator.validate(clauses);
If a clause contains a BinaryUnifier and this method has not been called, validate throws a DatalogValidationException with the message "Binary unification is not allowed".

​
Explicit disunification

The != operator, represented by the BinaryDisunifier AST node, requires that two terms are not equal. A body containing X!=Y succeeds only for substitutions where X and Y are bound to distinct constants. 
% Compute the pairs in tc where the source and destination differ.
distinct_tc(X,Y) :- tc(X,Y), X!=Y.
Disunification is a filter: it does not bind variables, it only prunes derivations where the two sides would unify. Both sides must already be bound by a positive body atom or a unification before the constraint is checked.

​
Enabling disunification in the validator

DatalogValidator validator = new DatalogValidator()
    .withBinaryDisunificationInRuleBody();

UnstratifiedProgram program = validator.validate(clauses);
If a clause contains a BinaryDisunifier and this has not been called, the validator raises "Binary disunification is not allowed".

​
Negation

The not keyword, represented by the NegatedAtom AST node, holds when the atom it negates is not provable given the current set of derived facts. This is the closed-world assumption: anything not explicitly derived is treated as false. 
% Derive every pair of nodes that are NOT in the tc relation.
node(X) :- edge(X,_).
node(X) :- edge(_,X).

not_tc(X,Y) :- node(X), node(Y), not tc(X,Y).
The node relation is necessary here to supply a finite domain for X and Y. Without it, the variables would be unbound — see the safety discussion below.

​
Safety rule for negation

Variables that appear inside a not atom are not bound by that atom. They must be bound by a positive body atom elsewhere in the same rule — either directly or through a chain of unifications.
The following rule is invalid and will be rejected by DatalogValidator:
% INVALID: X and Y are not bound by any positive body atom.
invalid_not_tc(X,Y) :- not tc(X,Y).
X and Y appear only inside the negated atom not tc(X,Y). Because negation does not bind variables, neither variable has a positive binding, violating the safety condition. The validator raises a DatalogValidationException identifying each unbound variable.The fix is to add positive atoms that bind X and Y first, as the not_tc example above does with node(X), node(Y).

​
Enabling negation in the validator

DatalogValidator validator = new DatalogValidator()
    .withAtomNegationInRuleBody();

UnstratifiedProgram program = validator.validate(clauses);
All three features can be combined on a single validator instance: 
DatalogValidator validator = new DatalogValidator()
    .withBinaryUnificationInRuleBody()
    .withBinaryDisunificationInRuleBody()
    .withAtomNegationInRuleBody();

​
Stratified negation

AbcDatalog supports stratified negation. A program is stratifiable when its predicate dependency graph has no cycle that passes through a negated edge — that is, no predicate can indirectly depend on the negation of itself. Stratification ensures that when a negated atom not p(X,Y) is evaluated, the relation for p is already fully computed. The evaluation proceeds stratum by stratum: all predicates whose definitions do not involve negation (stratum 0) are computed first, then predicates that depend negatively only on stratum-0 predicates (stratum 1), and so on.
Without stratification, negation can produce paradoxical or non-deterministic results. Consider a hypothetical rule p :- not p. — p holds if and only if p does not hold, which has no sensible semantics under the closed-world assumption.Stratified programs avoid this by guaranteeing that by the time the engine evaluates not p(...), the complete set of p facts has already been derived. The result is deterministic and well-defined: the perfect model semantics.AbcDatalog engines that support negation perform stratification as part of program initialization and will refuse programs that are not stratifiable.

​
Engine support

Not all AbcDatalog engines support these extended features. The following engines handle unification and stratified negation:

SemiNaiveEngine

Supports binary unification (=), binary disunification (!=), and stratified negation (not). This is the standard bottom-up semi-naive evaluation engine.

ConcurrentStratifiedNegationBottomUpEngine

A concurrent variant that evaluates strata in parallel where possible, also supporting unification, disunification, and stratified negation.
Always configure DatalogValidator to match the features your chosen engine supports before calling validate. Passing a program with unification or negation to an engine that does not handle those features will produce incorrect or incomplete results.

​
Complete example

The following excerpt from tc.dtlg demonstrates all three features together in a single program: 
% EDB
edge(a,b).
edge(b,c).
edge(c,c).
edge(c,d).

% IDB: transitive closure (linear recursion)
tc(X,Y) :- edge(X,Y).
tc(X,Y) :- edge(X,Z), tc(Z,Y).

% Unification: nodes that lie on a cycle
in_cycle1(X) :- tc(X,Y), X=Y.

% Disunification: tc pairs with distinct endpoints
distinct_tc(X,Y) :- tc(X,Y), X!=Y.

% Negation: node universe, then complement of tc
node(X) :- edge(X,_).
node(X) :- edge(_,X).
not_tc(X,Y) :- node(X), node(Y), not tc(X,Y).
Querying in_cycle1(X)? returns every node that can reach itself. Querying not_tc(X,Y)? returns every ordered pair of nodes (X,Y) for which no path from X to Y exists in the graph.

Build docs developers (and LLMs) love

Get started for freeTalk to us