Suppose I have the following scasp program that lets me know someone can do a demanding task if they are healthy:
:- use_module(library(scasp)).
:- use_module(library(scasp/human)).
% run:
% ?- human(demanding_tasks(X)).
:- pred demanding_tasks('X') :: '@(X:worker) can do demanding work'.
demanding_tasks(X) :- healthy(X).
healthy(john).
-healthy(delina).
human(Query) :-
scasp(Query),
scasp_justification(T,[]),
human_justification_tree(T).
Query:
1 ?- human(demanding_tasks(X)).
% the worker john can do demanding work, because
% healthy holds (for john), and
% The global constraints hold, because
% the global constraint number 1 holds, because
% there is no evidence that -healthy holds (for X), and
% -healthy holds (for delina), and
% there is no evidence that healthy holds (for delina).
X = john,
% s(CASP) model
{ demanding_tasks(john), not ¬ healthy(_A), ¬ healthy(delina), healthy(john)
},
% s(CASP) justification
query ←
demanding_tasks(john) ←
healthy(john) ∧
o_nmr_check ←
not o_chk_1 ←
not ¬ healthy(_A) ∧
¬ healthy(delina) ∧
not healthy(delina).,
_A ∉ [delina] ;
false.
I understand why the following three elements are in the model:
I’m still a beginner Here is my attempt. As we have a rule for -healthy/1, after proving john is healthy, we must prove that -healthy(john) does not hold (if it does, the model is inconsistent), so we get the call not -healthy(john). That could be solved without reasoning about -healthy(X). The way the constraint is implemented however is
:- healthy(X), -healthy(X).
This considers the entire domain of (un)healthy people, so we get -healthy(delina) into the model and must prove that healthy(delinda) is not hold. Now, not healthy(belinda) gets somehow not -healthy(X), X \= belinda. Here I am still a little stuck To some extend in helps to use this to print the generated query.
If you figure it out completely, please share. I do have the impression that classical negation can be handled more efficiently and we can produce better explanations for it. Joaquin is working on improving handling of global constraints. I do not know whether this also affects classical negation.
27 ?- scasp(healthy(X)).
X = john,
% s(CASP) model
{ healthy(john)
},
% s(CASP) justification
query ←
healthy(john) ∧
o_nmr_check. ; % no global consistency check generated
false.
Fact #2: If only a definite negative fact is present, the model integrity constraint is not triggered:
-healthy(delina).
29 ?- scasp(-healthy(X)).
X = delina,
% s(CASP) model
{ ¬ healthy(delina)
},
% s(CASP) justification
query ←
o_nmr_check. ; % no global consistency check here either
false.
Fact #3: If only a definite negative and positive facts/calls are present, the model integrity constraint are generated:
healthy(john).
-healthy(delina).
32 ?- scasp(healthy(X)).
X = john,
% s(CASP) model
{ not ¬ healthy(_A), ¬ healthy(delina), healthy(john)
},
% s(CASP) justification
query ←
healthy(john) ∧
o_nmr_check ←
not o_chk_1 ← % here we have the consistency checks
not ¬ healthy(_A) ∧
¬ healthy(delina) ∧
not healthy(delina).,
_A ∉ [delina] ;
false.
Why those specific global constraints?
Now let’s study each of the generated constraints, first the easy ones, then the hard one.
Why ¬ healthy(delina) and not healthy(delina) in the global constraints?
Because (in this case) the global constraints want to make sure the model is consistent (as Jan mentioned already). So a if an scasp program contains both definitely positive and definitely negative facts (or predicate calls), we need to make sure that if a definitely positive fact is asserted, then its definitely negative counterpart cannot be asserted also.
Explanation: This is common sense. If we state that delina is definitely not healthy (¬ healthy(delina)) then we must have no evidence that delina is definitely healthy ( not healthy(delina)), otherwise we would have an inconsistency; and that is why we have both global constraints present.
Interesting fact: these constraints are present regardless of the query or the rest of the program, because they need to guarantee the logical integrity of the program.
So far so good, this was what Jan explained before, but flushed out a little more. Now let’s get to the hard case, but before we do that, we have to understand negation in ASP/sCASP.
We first need to understand negation in sCASP (handling uncertain knowledge)
There are two types of negation in ASP:
1.1. not X means that we have no proof that X holds, in Prolog we usually see this as negation as failure. not healthy(delina)does not mean that delina is not healthy, it means that we can’t prove that she is healthy. In other words have we no evidence that she is healthy, but she --in fact-- could be healthy. (healthy(delina) would specify that she in fact is healthy).
1.2. -X (minus X) means that we know for sure that X does not hold. We don’t have this kind of negation in Prolog, and it is called classical negation. So -healthy(delina) means I know for sure that delina is not healthy.
Because we have these two kinds of negation we can express uncertain knowledge and what to do with it:
Expression
Meaning
Level of truth
healthy(delina)
Delina is healthy
Definitely true
not -healthy(delina)
No evidence that delina is unhealthy
Likelihood (that delina is healthy)
not -healthy(delina), not healthy(delina)
No evidence that delina is definitely unhealthy, no evidence that she is definitely healthy
Unknown
not healthy(delina)
No evidence that delina is definitely healthy
Likelihood (that delina is not healthy)
-healthy(delina)
Delina is not healthy
Definitely false
In order to handle negation in programs, ASP and sCASP generate dual rules for all predicates. A dual rule is the negation of the original rule. For example, with the following rules:
healthy(X) :- not sick(X).
healthy(X) :- doctor(D), not doctor_says_sick(D,X).
scasp would generate the following dual rules:
not healthy(X) :- not_healthy1(X), not_healthy2(X).
not_healthy1(X) :- sick(X).
not_healthy2(X) :- not doctor(D). % remember "not" means we don't have evidence
not_heatlhy2(X) :- doctor(D), doctor_says_sick(D,X).
If a call not Pred is made, then sCASP calls the corresponding dual rule to resolve the negation.
What about the variables involved? Now that we understand negation and duals, let’s look more closely what happens in this dual clause above:
not_healthy2(X) :- not doctor(D).
in the absence of any other clause, sCASP sees this as meaning there are no doctors. D is now universally quantified, because in the original program it was existentially quantified. In other words, the negation of doctor(D) when D is existentially quantified (as it is in the original clause), is that there are no Ds that satisfy doctor(D), for that reason ASP and SCASP introduce the sCASP forall mechanism, which would make not doctor(D) turn into not forall(D, doctor(D)).
(see slide 74 in Gupta’s great presentation ).
But the sCASP forall mechanism is quite smart, it can handle negatively constrained variables:
Suppose we have the following scasp program:
:- use_module(library(scasp)).
doctor(jan).
Now let’s ask sCASP for not doctor(D):
44 ?- scasp(not doctor(D)).
% s(CASP) model
{ not doctor(D)
},
% s(CASP) justification
query ←
not doctor(D) ∧
o_nmr_check.,
D ∉ [jan] ; % ALL values of D *except* Jan!
false.
Because of the internal forall mechanism and the ability to handle negatively constrained variables, sCASP was able to answer that the variable D can have any value, except jan. Quite useful and close to human thinking.
Back to the main problem: why "not ¬ healthy(_A), _A ∉ [delina] " in the global constraints?
Okay, now we’re back answering the original question. Let’s look at the original program:
healthy(john).
-healthy(delina).
32 ?- scasp(healthy(X)).
X = john,
% s(CASP) model
{ not ¬ healthy(_A), ¬ healthy(delina), healthy(john)
},
% s(CASP) justification
query ←
healthy(john) ∧
o_nmr_check ←
not o_chk_1 ← % here we have the consistency checks
not ¬ healthy(_A) ∧
¬ healthy(delina) ∧
not healthy(delina).,
_A ∉ [delina] ;
false.
Now let’s look at the global constraints that were generated:
47 ?- scasp_show(healthy(_), code(constraints(true))).
% QUERY:
% Query not defined
% USER PREDICATES:
-'user:healthy'(delina).
'user:healthy'(john).
global_constraints :-
global_constraint.
% INTEGRITY CONSTRAINTS:
not o__chk_1_1_vh1(Var0) :-
not -'user:healthy'(Var0).
not o__chk_1_1_vh1(Var0) :-
-'user:healthy'(Var0),
not 'user:healthy'(Var0).
not o__chk_1_1 :-
forall(Var0,not o__chk_1_1_vh1(Var0)).
not o_chk_1 :-
not o__chk_1_1.
global_constraint :-
not o_chk_1.
true.
As Jan said before, to make sure the model is consistent we have to make sure that healthy(X), -healthy(X) is always false for all values of X (but X could be negatively constrained). So let’s look at the constraints above:
not o__chk_1_1 :-
forall(Var0,not o__chk_1_1_vh1(Var0)). % this comes from the dual rule generated
% to handle the universal/existential quantification
% problem explained above
Now the implementation needed by the forall:
not o__chk_1_1_vh1(Var0) :- % Case #1
not -'user:healthy'(Var0). % If we don't have a -healthy(SomeX) we are okay:
% therefore, in the program we could either have
% healthy(SomeX) or nothing at all, everytihg consistent.
Now the next constraint:
not o__chk_1_1_vh1(Var0) :-
-'user:healthy'(Var0), % make sure this is not Case #1 above
not 'user:healthy'(Var0). % if we have -healthy(SomeX) we cannot
% have healthy(SomeX)!
Great, this insures the consistency of the model. So where did "not ¬ healthy(_A), _A ∉ [delina] " come from?
From the first clause of o__chk_1_1_vh1 above:
not -'user:healthy'(Var0).
This is similar to our not doctor(D) example above, which told us that D could be any value except jan, so here we have the answer: Var0 can be any value except delina, and therefore we have "not ¬ healthy(_A), _A ∉ [delina] " in the model.
Quite amazing
What is the meaning of "not ¬ healthy(_A), _A ∉ [delina] "? It is telling us that in our program (not for our specific query, but as a requirement for our whole program) we could add facts of the form healthy(SomeX)as long as the SomeXs are not delina. In other words, it is telling us HOW WE COULD MODIFY OUR PROGRAM, while keeping it consistent! It is telling us a possible compatible FUTURE STATE OF THE WORLD modeled by the program. WOW!! Sorry I had to bold and write in all caps, but that is quite amazing! Just simply amazing. I just don’t cease to marvel at this beauty!
That was a long answer, but it was a hard problem that needed much background. I am so amazed by sCASP capabilities to handle human-like knowledge that I wanted to share all this with the community. No one should miss this great work.
I would like to give more than one “like” This is a great write up. 90% was already in my head but this puts it all together and fills in a few details.
s(CASP) adds the constraint (false) :- healthy(X), -healthy(X), proving the constraint for any X regardless of the model (@swi). This however seems an overkill to me. It seems good enough to merely prove that healthy(john) doesn’t hold and leave belinda out of the equation. If the user would be interested in models that are consistent for all healthy(X), s/he could add the above generalized constraint to the program.
In other words, instead of what happens now, we could rewrite the above into
demanding_tasks(X) :- healthy(X), not -healthy(X).
healthy(john).
-healthy(delina).
And not generate a global constraint. We can simulate that using the --no_nmr option and get the model
{ demanding_tasks(john), healthy(john), not -healthy(john) }
I don’t think it is a good idea to eliminate the global constraints that guarantee the consistency of classical negation. It is the principle of non-contradiction that needs to hold here. However, I do think it would be okay to provide an option to prevent the generation of the global constraints for p(X),-p(X) in case the user wants it.
The reason is that ASP’s essence is to give back the user an answer set, and not simply to answer a query (by binding variables) as in prolog. In fact, from my reading it seems to me that goal directed solving of ASP programs was developed a little later (see slide 63 in the Gupta presentation linked above).
I suspect eliminating those global constraints could make the whole system unstable; not for simple facts like we are dealing with here, but when we have more complex programs. Much like the reason you had before for not specializing the queries, and keeping them generalized.
Interesting. I’m not completely convinced (yet). One of the claims of goal directed ASP is to only consider the “relevant” part of the program. There are several reasons that make this attractive
It keeps the explanation small
It keeps the model small
It saves time
(It avoids getting no model due to unrelated code)
The latter is between () because I’m not sure about it. I think It does make sense though, particularly when the aim is human style reasoning. When I’m reasoning about what I’ll do after finishing this email I consider preferences and constraints while ignoring problems that are unrelated It is also one of the claims from the WFS (Well Founded Semantics) people that WFS can from the same program provide true, false and undefined atoms. The last category depends on an inconsistent program fragment.
Using local constraints to ensure consistent classical negation surely contributes to the four points above.
Well, I hear the s(CASP) people are planning to set up a Discourse forum, so we can easily communicate with all of them!
Here is my attempt. As we have a rule for -healthy/1, after proving john is healthy, we must prove that -healthy(john) does not hold (if it does, the model is inconsistent), so we get the call not -healthy(john). That could be solved without reasoning about -healthy(X). The way the constraint is implemented however is
To some extend in helps to use this to print the generated query.
We first need to understand negation in sCASP (handling uncertain knowledge)
Back to the main problem: why "
Quite amazing