Problem with sCASP dual programs

my code on swish looks like this:

% s(CASP) Programming
:- use_module(library(scasp)).
%:- style_check(-discontiguous).
:- style_check(-singleton).
%:- set_prolog_flag(scasp_unknown, fail).

% Your program goes here

% sCASP encoding of rps
% Reference: Jason's article at

#pred player(X) :: '@(X) is a player'.
#pred participate_in(Game,Player) :: '@(Player) participated in @(Game)'.
#pred winner(Game,Player) :: '@(Player) is the winner of @(Game)'.
#pred throw(Player,Sign) :: '@(Player) threw @(Sign)'.
#pred beat(Sign,OtherSign) :: '@(Sign) beats @(OtherSign)'.
#pred game(G) :: '@(G) is a game of rock-paper-scissors'.


winner(Game,Player) :-
  Player \= OtherPlayer,

  % There is a Game in which Bob and Jane played.

  /** <examples> Your example queries go here, e.g.
  ?- ? winner(testgame,Who).

If I run the query ?- ? not winner(testgame, bob)., I get the expected result, which is no models. If you modify the code to make the disequality the last line of the winner rule, it returns one incorrect model.

I tried the same code in the Ciao implementation of s(CASP) and got essentially identical results, so it doesn’t seem like an issue with the port. If anything, SWISH produced the incorrect result must more efficiently. :slight_smile:

Here’s the model SWISH gives:

? not winner(testgame,bob).
s(CASP) model
testgame is a game of rock-paper-scissors
there is no evidence that A not bob, or jane is a player
bob is a player
jane is a player
there is no evidence that rock beats rock
bob participated in testgame
there is no evidence that bob threw B other than rock
there is no evidence that bob threw C other than rock
there is no evidence that bob threw D other than rock
bob threw rock
there is no evidence that bob is the winner of testgame

The dual program generated by Ciao scasp when you run scasp --code includes, as the next-to-last definition of the predicate, when the disequality is last in the clauses:

not o_winner_1(Var0,Var1,Var2,Var3,Var4) :-
     not beat(Var3,Var4).

I think this is the version of the rule that is getting triggered, because it is the only one with not beat included, and not beat(rock,rock) is in the resulting model.

It’s incorrect because it is excluding the one remaining condition, the disequality. If you haven’t considered whether or not the two players are allowed to be the same player, then the fact that the player doesn’t beat themselves doesn’t mean the person didn’t win.

I think the problem is the way the duals are constructed. not o_winner_1/5 is defined several times, each time adding just one of the original clauses, negated. In every subsequent definition, anything added previously is kept, but no longer negated.

So if the original rule is:

1 :- 2, 3, 4.

you get

not 1 :- not 2.
not 1 :- 2, not 3.
not 1 :- 2, 3, not 4.

It seems to me that it would be more correct if we got something like this:

not 1 :- not 2, 3, 4.
not 1 :- 2, not 3, 4.
not 1 :- 2, 3, not 4.
not 1 :- not 2, not 3, 4.
not 1 :- 2, not 3, not 4.
not 1 :- not 2, not 3, not 4.

Let me know if I’m out to lunch. Fighting with s(CASP) to make duals work properly was my least favourite part of dealing with it last year. Would be great to improve on that.

This excellent example of the problem was brought to my attention by Eric at this medium reply.

1 Like

If the dual would be like in the Clark completion, and lets only
consider a binary conjunction. Then the dual of:

p :- q, r.

Would be:

~p :- ~q; ~r.

Lets check whether they are equal to either:

~p :- ~q
~p :- q, ~r.

Or then:

~p :- ~q, r.
~p :- q, ~r.
~p :- ~q, ~r.

Here are the results, whether they are the same:

((¬q ∨ ¬r) → ¬p) ↔ ((¬q → ¬p) ∧ ((q∧¬r) → ¬p)) is valid.
((¬q → ¬p) ∧ ((q∧¬r) → ¬p)) ↔ (((¬q∧r) → ¬p) ∧ (((q∧¬r) → ¬p) ∧ ((¬q ∧ ¬r) → ¬p))) is valid.
(((¬q∧r) → ¬p) ∧ (((q∧¬r) → ¬p) ∧ ((¬q ∧ ¬r) → ¬p))) ↔ ((¬q ∨ ¬r) → ¬p) is valid.

Just enter the formulas here, and check whether you always get T:

I’ve sent a mail to Joaquin to make him aware of this post

That is in interesting concept :slight_smile: I’m not that deep into this stuff. I guess we need these conjunctions because the literals are not ground and thus e.g., not 3 may only hold if 2 holds. In the ground scenario we get @j4n_bur53’s translation.

1 Like

Hi all,
For generating duals both approaches have pros and cons.
There are more details in page 6.
You can obtain the “binary conjunction” by using the flag -d or --plaindual.

As for rock-paper-scissors, and in general for predicate programs, the order of the literals matters. Note that the disequality constraint is used to prune the case where both players are the same.

In summary, dual generation in predicate programs introduces an optimization to eliminate redundant answers/justifications.



What I’m gathering is that my proposal above is logically equivalent to what s(CASP) does with plainduals, which solves my problem but has a different problem of generating extra justifications (and correspondingly slowing the processing time) for default negated terms wherever they occur in the search.

Let me know if that’s close.

If the performance hit from plainduals is not tolerable, and I anticipate it might not be, I will need some sort of guidance on how to avoid this pitfall going forward. My approach right now is unsophisticated and time consuming.

Does it happen only to disequalities, or can other things trigger it like default negations and constraints? Does it depend on the absolute position in the clauses, or the relative position to some other clause? Does it matter whether the clause is being used to “prune” the search? What rule of thumb can I follow that will avoid the issue? If anyone has such guidance off-hand, please let me know.

I have a suspicion there may be interesting parallels to some natural language expressions used in legislation, but we’ll see.

If no one is sure, I’ll try to figure it out and let everyone know what I come up with.

Thanks for all the help. Greatly appreciated. Would be nice to have that s(CASP) forum to ask these questions in, rather than forcing Joaquin to respond in multiple places… did we ever make any progress on that?

1 Like

OK, so here’s my thinking on it so far…

In s(CASP), your rules are defining both the positive and the default negative at the same time. Because of the way the duals are generated, you should only include a condition if:
a) it is a necessary condition of the predicate being true, and
b) its reversal in the dual program is a sufficient condition of the predicate not holding, given the conditions above it holding.

If a) and b) are not both true, adjust the clause order until they are.

That is still too complicated for me. Here’s version two:

Only include a clause if
a) it is a necessary condition of the predicate being true, and
b) its reversal is a sufficient condition of the predicate not holding.

If you have a clause that meets a) but doesn’t meet b), reformulate by adding predicates until they all satisfy both.

(I have known for a while that changing the number of predicates has fixed things for me. This may be why?)

Following this advice, the original predicate:

winner(Game,Player) :-
  player(Player), % Ungrounded only works if the disequality is below here
  throw(Player,Sign), % not winner/2 only works if the disequality is above here.

Is wrong because not_same_player is a necessary condition, but the opposite is not sufficient to show that anyone didn’t win a game. That bob is bob does not mean that bob didn’t win.

Note that not_same_player(X,Y) :- X \= Y., and is used just to be able to add a plain-language version to the justifications.

So we reformulate, putting the disequality into a predicate for which both things are true:

game_has_two_different_players(Game,Player,OtherPlayer) :-

winner(Game,Player) :-

A game having two different players is a necessary condition of it having a winner, and that not being true is sufficient for us to know there is no winner. The disequality is a necessary condition of the game having two players, and two players being the same is sufficient is sufficient to show that the predicate does not hold for those two players.

So everything behaves as expected in both the positive and default negated cases.

Line order still matters, because the disequailty needs to be placed after at least one of its terms has been bound, I think, but that’s a different thing.

Does that seem like it follows? Can you think of examples of places where this kind of reformulation isn’t available?

Is the reformulation actually solving the problem, or am I getting the right result but misunderstanding how? I note that all of the variables in game_has_two_different_players appear in both the head and the body. Maybe that is solving the problem, somehow?

Thanks again.


Having thought about it further, it occurs to me that both adding variables to the conclusion and adding intermediate predicates to the body are examples of ensuring that the negations of all of the conditions are sufficient for the negation of their conclusion. It’s two sides of the same coin.