<div class="notebook"> <div class="nb-cell markdown" name="md1"> # s(CASP): Abduction over disunity A demonstration of a problem I'm having using abduction in s(CASP) in SWI-Prolog </div> <div class="nb-cell program" data-background="true" name="p1"> :- use_module(library(scasp)). % Uncomment to suppress warnings :- style_check(-discontiguous). :- style_check(-singleton). :- set_prolog_flag(scasp_unknown, fail). </div> <div class="nb-cell markdown" name="md2"> ## Problem I want to be able to use abductive reasoning across rules that require disunity. So for example, I want to be able to say that the winner of a game of rock paper scissors is known if there are two different players. </div> <div class="nb-cell program" name="p2"> winner(Game,Winner) :- game(Game), player(Winner), player(Loser), Loser \= Winner, participant(Game,Winner), participant(Game,Loser), threw(Winner,Sign1), threw(Loser,Sign2), beats(Sign1,Sign2). game(testgame). player(bob). player(jane). participant(testgame,bob). participant(testgame,jane). threw(bob,paper). threw(jane,rock). beats(rock,scissors). beats(scissors,paper). beats(paper,rock). </div> <div class="nb-cell query" name="q1"> ? winner(testgame,X). </div> <div class="nb-cell markdown" name="md3"> If I try to do the same thing making all of the inputs abducible, it doesn't work. </div> <div class="nb-cell program" name="p3"> winner(Game,Winner) :- game(Game), player(Winner), player(Loser), Loser \= Winner, participant(Game,Winner), participant(Game,Loser), threw(Winner,Sign1), threw(Loser,Sign2), beats(Sign1,Sign2). #abducible game(X). #abducible player(X). #abducible participant(X,Y). #abducible threw(X,Y). beats(rock,scissors). beats(scissors,paper). beats(paper,rock). </div> <div class="nb-cell query" name="q2"> ? winner(testgame,X). </div> <div class="nb-cell markdown" name="md4"> If I remove the disunity, it works. </div> <div class="nb-cell program" name="p4"> winner(Game,Winner) :- game(Game), player(Winner), player(Loser), %Loser \= Winner, participant(Game,Winner), participant(Game,Loser), threw(Winner,Sign1), threw(Loser,Sign2), beats(Sign1,Sign2). #abducible game(X). #abducible player(X). #abducible participant(X,Y). #abducible threw(X,Y). beats(rock,scissors). beats(scissors,paper). beats(paper,rock). </div> <div class="nb-cell query" name="q3"> ? winner(testgame,X). </div> <div class="nb-cell markdown" name="md5"> It also works if there is at least one of the disunified variables that binds with something. </div> <div class="nb-cell program" name="p5"> winner(Game,Winner) :- game(Game), player(Winner), player(Loser), Loser \= Winner, participant(Game,Winner), participant(Game,Loser), threw(Winner,Sign1), threw(Loser,Sign2), beats(Sign1,Sign2). #abducible game(X). #abducible player(X). #abducible participant(X,Y). #abducible threw(X,Y). player(bob). beats(rock,scissors). beats(scissors,paper). beats(paper,rock). </div> <div class="nb-cell query" name="q4"> ? winner(testgame,X). </div> <div class="nb-cell markdown" name="md6"> But the requirement is not "at least one", it is "no more than one missing". This is as close as I have gotten to undersatnding the problem. Regardless of how many different bindings for p(X) a rule requires, s(CASP) hypothesizes at most one. </div> <div class="nb-cell program" name="p6"> there_are_three :- thing(A), thing(B), thing(C), A \= B, B \= C, A \= C. #abducible thing(X). </div> <div class="nb-cell query" name="q5"> ? there_are_three. </div> <div class="nb-cell program" name="p10"> there_are_three :- thing(A), thing(B), thing(C), A \= B, B \= C, C \= A. #abducible thing(X). thing(first). </div> <div class="nb-cell query" name="q9"> ? there_are_three. </div> <div class="nb-cell program" name="p7"> there_are_three :- thing(A), thing(B), thing(C), A \= B, B \= C, C \= A. #abducible thing(X). thing(first). thing(second). </div> <div class="nb-cell query" name="q7"> ? there_are_three. </div> <div class="nb-cell markdown" name="md7"> One work-around that I have considered is just manually abducing the existence of things up to a certain number. But this adds global constraints to everything, complicates the models, and messes up the way the abudction is displayed in the explanations. </div> <div class="nb-cell program" name="p8"> winner(Game,Winner) :- game(Game), player(Winner), player(Loser), Loser \= Winner, participant(Game,Winner), participant(Game,Loser), threw(Winner,Sign1), threw(Loser,Sign2), beats(Sign1,Sign2). #abducible game(X). #abducible participant(X,Y). #abducible threw(X,Y). #abducible option(1). #abducible option(2). #abducible option(3). #abducible option(4). #abducible option(5). create_at_least(2). -player(X) :- not player(X), option(X), X #=< Y, create_at_least(Y). player(X) :- not -player(X), option(X), X #=< Y, create_at_least(Y). beats(rock,scissors). beats(scissors,paper). beats(paper,rock). </div> <div class="nb-cell query" name="q6"> ? winner(testgame,X). </div> <div class="nb-cell query" name="q8"> ? player(X). </div> </div>