Negation in chr program

Hi.
I’m working on adding chr to a program for abductive reasoning. I use this to ask what conditions are necessary for a predicate to be true.
Up to now the program made use of negation as failure to consider unproven facts as false, but with chr it doesn’t work.

A simple example:

:- use_module(library(chr)).					

:- chr_constraint professor/1, rich/1, has_student/2.
professor(X), rich(X) ==> fail.

happy(X):- rich(X).
happy(X):- professor(X), has_good_students(X).

has_good_students(X):-
    \+ has_student(X, bad_student).

In my mind this should have answered with two possibilities to the query happy(bob):

  • rich(bob)
  • professor(bob), not has_student(X, bad_student).

The second option is missing. I must be missing something.
It’s the first time I reason with chr.

CHR constraints do not behave as normal predicates. If you run listing(has_student), you’ll not see facts you stated, eg. has_student('bob', 'peter'). Instead there’s a pretty cryptic chunk of code that wires the constrained variables with frozen goals that later apply the constraint rules. So \+ has_student(X, bad_student) does not check if there is a bad student, it states that there should be one within a negation, which fails because there’s nothing to disprove it.

You can achieve what you want by doing this instead:

has_good_students(X), has_student(X, bad_student) ==> false.

So that running has_good_students(X) will constrain X so that later running has_student(X, bad-student) will fail.

Thanks!
Is it possible to have something like not has_student(X, bad_student) in the solutions?
If I run happy(X) I get the following:

rich(mario) ;
professor(mario),
has_good_students(mario).

I would like to have it say:

rich(mario) ;
professor(mario),
+ has_student(mario, bad_student).

I don’t think there’s a generic way to do this. I don’t see any form of negation supported by CHR system provided by SWI Prolog and from what I understand CHR rules are isolated per-module, so there’s probably no way to implement a generic operator.

Closest you could get is write a negated constraint has_not_student/2 yourself:

has_not_student(X, S), has_student(X, S) <=> false.
has_good_students(X) <=> has_not_student(X, bad_student).

Thanks @AmbientTea . This seems to be close to what I intended.
Just one more thing…
The code is now:

:- use_module(library(chr)).					

:- dynamic has_student/2.

:- chr_constraint professor/1, rich/1, has_student/2, has_good_students/1, has_student/1, not_has_student/2.
professor(X), rich(X) ==> fail.

% Exception in CHR.
not_has_student(X, S), has_student(X, S) ==> false.
has_good_students(X) <=> not_has_student(X, bad_student).

happy(X):- rich(X).
happy(X):- professor(X), has_good_students(X).

If I load this file and run assert(has_student(bob, bad_student) and query happy(bob) I still get has_good_students(bob) as a possible solution.
But it should not be true.

If you intend to assert has_student as a fact then it should not be a CHR constraint. Constraints are put on variables to limit how these variables can be instantiated in the future and they’re not asserted, they’re called like normal predicates.

I recognize the example that I introduced in the CHR Summer School, 2010 I think, and used in a few later publications :wink:
This sort of “explicit negation” for abduction with CHR is introduced and analyzed in the paper about HYPROLOG (together with V.Dahl, 2005). When you declare an abducible, say a/1, its “negation” a_/1 is automatically introduced together with the rule a(X), a_(X) <=> false. Why it is not exactly negation is that you miss the axiom a(X) / a_(X) which cannot be expressed decent ly in CHR plus Prolog. Well, if you have time enough to wait for immense backtracking, you can add a prefix to you query consisting of (a(monkey);a_(monkey)) and so on for all possible instances of the abducible a/1 (!!). The theoretical background for this way of doing abduction with CHR is spelled out in a few other papers (first paper in this direction dates to 2000)
– I’d be happy to hear more about your research on abduction with CHR

Thanks for the help! I did in fact read the hyprolog paper, and I’m building a small demo of my knowledge base with it. It does simplify things considerably coming from pure chr.
The issue is that my rulebase (a set of legal norms) is getting quite large, and makes heavy use of negation as failure, as in, if the user did not assert a certain fact, it can be considered false in the set of things we know about the user.
The main issue is that I cannot use the “normal” negation (+) in a chr program, as it seems to be mostly ignored.
I need to find a way to express the concept of a negation (i.e. a fact that is omitted) but can be implemented as abducible), and an exception (i.e. a negation that is expressed as a prolog statement, that relies on other facts.
I’m not sure I clarified my intentions, I might rewrite all this paragraph a couple of times again :wink:

Hi,

hyprolog sounds very interesting. I looked up the paper but its pretty technical.

Could you perhaps post a short didactic example, to illustrates its use and utility.

thanks,

Dan

Glad to be of help :slight_smile:
If you only negate facts one at a time (in HYPROLOG, abducibles), I think the explicit negation will do. If you test the negated fact_(7), it will succeed if fact(7) is not present, and any later attempt to test fact(7) will fail.
I did try to once to include recursion through negation, i.e. turning conjunctions to disjunctions etc., and with general unification it became a terribly complicated mess - so gave that up.
Please keep me posted

I think you can find such examples at the website, the users guide has a few minimalist examples, and the sample programs are more developed. HYPROLOG: Abduction and Assumptions in Logic Programming

1 Like

I made a simple example of what i mean using the wet grass example.

abducibles rained_last_night/0, grass_is_covered/0, tuesday/0.

grass_is_wet:- rained_last_night, \+ exception.
grass_is_wet:- sprinkler_was_on.
sprinkler_was_on:- tuesday.
exception:- grass_is_covered.

In this case I have a general rule, and an exception to that rule.
The execption itself cannot be an abducible, but the conditions for which the exception applies can.
What I would need is the ability to query
grass_is_wet, and have the system return something similar to:

rained_last_night, grass_is_covered_;
tuesday.

But at the moment I only get the second response, since the first is stopped on the negation.

I think the program is incorrect wrt. to the intuition you want to describe. And as you notice \+ does not do the work (deeply rooted in the nature of Prolog, it is impossible to export anything from a call to \+).
I would express the thing as:

abducibles rained_last_night/0, grass_is_covered/0, tuesday/0.

grass_is_wet:- rained_last_night, not_exception.
grass_is_wet:- sprinkler_was_on.
sprinkler_was_on:- tuesday.
not_exception:- grass_is_covered_.

What I did was to rewrite the clause exception:- grass_is_covered. manually (but systematically) into a clause for its negation. It works nicely in this simple example, but of you have something more complicates like
exception:- a, b.
exception:- c, d.
(a,b,c,d being abducibles).

In this case, you can write:

not_exception:- (a_ ; b_), (c_, d_).

I.e., when negating disjunctions become conjunction and vice versa.

Last clause should be
not_exception:- (a_ ; b_), (c_ ; d_).

Yes, In fact I tried changing all the exceptions in not_exception.
It works in simple examples, but it can become fairly complicated when dealing with multiple exceptions.
Also, in my system I need to be able to either work with abducibles, or with grounded terms, depending on the query. so it might be that I know it is not tuesday (as in the previous example),