Soundness with regards to the credal semantics

[David-Tuc]

Hello,

I would like to point out a soudness issue wrt the Credal Semantics that does not seem to have been addressed in the paper Statistical Statements in Probabilistic Logic Programming.

While you check here for the consistency of the program, this check is done after constraining the probabilistic facts.

As such a program as the following:

0.5::a.
:- a.
b.
query(b).

gives p(b) =0.5 while this program does not have a Credal Semantics. This is the case for the program mky as well, which is why PASOCS could not output any probabilities.

Best

[damianoazzolini]

Hi, you are indeed right, and the software is not well documented yet. There is a flag, -sif (that stands for 'stop if inconsistent') that you can set. For example, with the previous program, if you don't add any flag you get 0.5, which is not correct. However, if you use the -sif flag: python3 pasta_solver.py temp.pl --query="b" -sif you get

Error: found 1 worlds without answer sets: [1]
1{ a }

By default is off and we assume that the program has indeed a credal semantics (every world has at least one stable model). Hope this helps.

[David-Tuc]

Hi,

Thanks for the details !

From the source code, the flag -sif seems to check if you actually got at least an answer set for each total choice when computing the probability, not if the program before adding the constraint is consistent. When running with the -sif flag, I get an error with the following program:

0.5::a.
b :- a.
query(b).

which should be fine.

This seems to affect the learning as well, as for example the set of abduced atoms in the smoking example gives a program with no Credal Semantics.

[damianoazzolini]

The pipeline is as follows: first we convert the PASP program into an ASP program (so 0.5::a is converted into {a}) and then we compute all the projected answer sets. So we consider the constraints as part of the program from the beginning, we consider everything as a whole. If we want to check that every world has at least one answer set, we go through all the computed answer set and we actually check this. So the answer set computation always take place. We do not check the property before the computation. Does this answer your question? Please let me know if it is still not clear.

The flag -sif should always be used with the flag -nm (no minimal set). This is not explained (thanks for pointing this!). The minimal set is the set of probabilistic facts that should always hold to make the query true. Note that this minimal set makes sense only if the program has at least one model for every world (if not, the elements of this set are not correct). We can identify the probabilistic facts in the minimal set by running cautious consequences on the ASP version of the program. In your example, this minimal set contains a (since a must be true to make the query true), so we add :- not a. in the program. In this way, this coverted program does not have a credal semantics, but the original one does have it. However, the probability we get from the program with the constraint is the same as we get with the original program, but we generate olny 1 world instead of 2. Thus, if you only use -sif, the solver will check the consistency of the program with the constraint, thus fails. Hovever, when -nm is used, the minimal set is not computed, so the program is unchanged.

python3 pasta_solver.py temp.pl --query="qry" -sif -nm
Lower probability == upper probability for the query: 0.5

You can try the flag --pedantic to see the whole converted program and the minimal set.

For the abduction task, you actually spot a bug in the condition :) the error is in the if condition before the print error, I will fix it as soon as possible! Thanks again, please let me know if you spot something else ore something is not clear! Note that some of the options are still unimplemented or only in a very early stage. The one that should work are the one described in the papers (so only abduction and exact inference at the moment).

[David-Tuc]

So the answer set computation always take place. We do not check the property before the computation. Does this answer your question? Please let me know if it is still not clear. Sorry about not being clear about that. I meant that the check happens after computing the minimal set of PFs necessary. Not computing the minimal set with -nm computes all the answer sets no ?

I believe that the issue with the smoke is in the translation of the constraint, one world gives the following program:

fe(a,b).
fe(a,d).
fe(e,c).
friend(X,Y):- e(X,Y), fe(X,Y). 
friend(X,Y):- e(Y,X), fe(Y,X).
smokes(b).
smokes(d).
smokes(X) ; no_smokes(X):- friend(X,Y), smokes(Y).
ic :- #count{X:no_smokes(X)} = N, #count{X:smokes(X)} = S, 10*S<8*(N+S).
:- f, ic.
:- not f, not ic.
query(smokes(c)).
e(b,c).
e(d,e).
e(e,c).

Which is unsatisfiable.

I'm still trying to understand the concept of probabilistic IC and the translation done. Especially :- not f, not ic., as it seems to forces the "inverse" constraint whenever PF for the constraint is false. I'll continue playing around with it, thank you for your help 👍

[damianoazzolini]

Yes, the consistency check happens after the computation of the minmal set. And this is currently the only way to do it. With the flag -nm, the software computes all the projected answer sets (wich is very likely that are less than the total number of answer sets).

Regarding abduction, first notice that probabilistic ICs are only supported when the flag --abduction is used. In the case the program is inconsistent, we simply discard the choice of abducibles.

Regarding the conversion, consider that ICs impose that the body must be false. So the rule ic:- body must be false if the IC is selected. The IC is selected when its probabilistic fact f is selected. So, if f is true, the IC is selected and the rule must be false (:- f, ic.). Likewise, if f is false the IC is not selected, and the rule must be true (:- not f, not ic). Let me know if this makes the process a little bit more clear, and do not hesitate to contact me if something is still unclear. Thanks.

[damianoazzolini]

Hi, I've pushed some modifications. Now the program stops if the PASP program is inconsistent, by default. I suggest closing the issue. Do not hesitate to contact me if something is still unclear. I'm currently fixing the abduction task and working on the semantics of probabilistic integrity constraints. I will let you know when it will be fully ready.