[INFO] Implementing conventional NAF(negation as failure) in s(CASP)

[jinulee-v]

In case of anyone seeking to modify s(CASP) to follow well-known NAF semantics,

To implement conventional Negation As Failure(NAF) semantics, two changes are required:

• solve_goal_predicate/8 should handle Goal = not(_) and Goal \= not(_) seperately,
• and all foralls in the dual statement should be removed via comp_dual/2.

1. New solve_goal_predicate for negated literals

• First, when encountering not(_), first attempt to solve the positive literal.
• If it fails, proceed with the original dual statement.

solve_goal_predicate(Goal, M, Parents, ProvedIn, ProvedOut, StackIn, StackOut,
                     GoalModel) :-
    Goal = not(InnerGoal),
    verbose(format('innergoal: ~p ~n', [InnerGoal])),
    (solve_goal_predicate_(InnerGoal, M, Parents, ProvedIn, _, StackIn, _, _)
    ->  fail % If its positive dual suceeds, fail the proof.
    ;   solve_goal_predicate_(Goal, M, Parents, ProvedIn, ProvedOut, StackIn, StackOut, GoalModel) % Proceed on dual statements
    ).

(solve_goal_predicate_ is the original solve_goal_predicate/8 renamed without modification.)

2. Remove foralls in dual statement in comp_duals.pl:157:

comp_dual2(Hn, Bg, Bv) :-
    Hn =.. [F|A1],
    append(A1, Bv, A2),
    length(A2, Arity),
    split_functor(F, Base0, _), % remove arity
    atomic_list_concat([Base0, '_vh', Arity], Base),
    join_functor(F2, Base, Arity),
    Hn2 =.. [F2|A2], % add body variables to innermost head.
    % define_forall(Hn2, G, Bv), % get the call to the innermost dual
    comp_dual3(Hn2, Bg, []), % create innermost duals
    c_rule(Rd, Hn, [Hn2]), % create dual
    assert_rule(dual(Rd)).