Thanks for the detailed explanation!
So, a quick workaround would be to trick the translator into believing that the
positive of the derived Q predicate is relevant. I tried this, by adding a dummy
operator identical to the existing set-p except it has an extra parameter ?y and
the precondition (secondary-q ?y). This problem is indeed solvable :)
I don't think it's for me to tell you how to solve the problem, but it seems
that keeping the translation mechanism simple and correct (and, if necessary,
computing the reformulated axiom set on demand, storing it separately, and using
where it is helpful) would be a more modular solution. Working out the
semantically correct way of reasoning about negative axioms - particularly in a
relaxed setting - is indeed interesting (in fact, that's the reason we're now
looking at these problems...) but also possibly quite tricky. I'm not sure if it
can be done in standard logic, or if it requires something else (like
well-founded semantics/answer-set programming, etc). |