Making a set of inference rules "proper"

Given this set of inference rules:

p <- a, b
~a <- ~a
~b <-
s <- ~p

where the set of candidate assumptions is {a, b, ~p}

In trying to make this set of rules "proper" by taking into account the finer details, I came up with this:

p <- a, b
not_a <- not_a, c
not_b <- d
s <- e

where
the set of candidate assumptions is {a, b, c, d, e}
and the contrary relations are
~a = {not_a}, ~b = {not_b}, ~c = {a}, ~d = {b}, ~e = {p}

Is this correct? In particular, I'm not sure whether the rule 'not_a <- not_a, c'
captures the loop of '~a <- ~a', and whether the contrary of 'c' should be {a} or
something else.

You have introduced far too many elements in your translation, it would have been sufficient to say:

p <- a, b
~a <- ~a
~b <-
s <- ~p

where {a,b,~p} are assumptions with contraries ~a, ~b, p respectively.

Please do not forget that the underlying deductive system can be anything, and the only requirement on assumptions is that they do not occur as conclusions of rules, so the above is a perfectly legitimate assumption-based framework that makes our point.

If you would like to avoid the use of ~ (which is fine), you could have

p <- a, b
not_a <- not_a
not_b<-
s <- not_p

where {a,b,not_p} are assumptions with contraries not_a, not_b, p respectively.

You can see that the only difference with the above is purely syntactic.