it looks like it doesn't handle negation. one of those unfortunate but interesting features of the space of recursive declarative languages.
if you allow something to be true only if something else is not true, your solution space is no longer monotonic. meaning that a result you thought was part of the solution can later be retracted. if there is a cycle (trivially "a if not a"), then you may not ever arrive at an answer. that might seem simple to detect, but that cycle can exist through an arbitrary number of rules and data dependencies, so in the limit is undecidable.
ideally, as in this solver, you could keep adding terms you could show to be correct from the data and rules at hand until they and all their consequences have been found, and which point you can stop (fixed point). but negation screws up this plan.
there are various restrictions on negation, solver heuristics, and partial conservative proofs of termination that can be applied. but this is where your beautiful simple declarative world starts getting sad and messy.
[edit: I'd like to leave this because I wish I understood the problem with negation earlier, but I just skimmed and missed stratification, Frank thoughtfully explains below]
I'm drinking at the moment, so maybe messy but not sad.
The engine supports negation in the standard way: stratification. You can call 'from_antijoin' with a static relation for its second argument but not a variable. It is not discussed in the post because it is a bit of a diversion from the intended message (and because antijoin is computationally not much different from a filter).
If you would like a more general compute model with non-monotonic iteration, I recommend differential dataflow!
if you allow something to be true only if something else is not true, your solution space is no longer monotonic. meaning that a result you thought was part of the solution can later be retracted. if there is a cycle (trivially "a if not a"), then you may not ever arrive at an answer. that might seem simple to detect, but that cycle can exist through an arbitrary number of rules and data dependencies, so in the limit is undecidable.
ideally, as in this solver, you could keep adding terms you could show to be correct from the data and rules at hand until they and all their consequences have been found, and which point you can stop (fixed point). but negation screws up this plan.
there are various restrictions on negation, solver heuristics, and partial conservative proofs of termination that can be applied. but this is where your beautiful simple declarative world starts getting sad and messy.
[edit: I'd like to leave this because I wish I understood the problem with negation earlier, but I just skimmed and missed stratification, Frank thoughtfully explains below]