Negative relations

[bvssvni]

For example:

(capital_missing_country, X) :- Y : country, X : capital, !(Y, X).

Negative relations should be in their own list at the end of the rule, such that a counter-proof can be searched for using a modification of normal rules.

It works by first matching on the rule like normal for positive terms. When there are only negative terms left, the first term is looked for as normal, but the new reduced expression is not added. Instead, the negative terms are just filled in:

(capital_missing_country, x) :- !(y, x).

Then, a linear solver is used to remove all expressions with variables in the negative terms that are covered. Finally, the linear solver lifts the remaining expressions that have variables at the right side.

The lifted expressions are added as new facts to the original facts, and then the monotonic solver is run again. If the monotonic solver proves ambiguity then inconsistency can be detected. The monotonic solver must prove all facts it proved in the previous round.