I've been trying to detect if a formula is not a consequence of some assumptions (i.e. if `A -> B` is not the case). This particular question represented an issue to me, as long as I wanted to separate the some-kind-of-solid logic language definition from dirty programming tricks.
I think there is a thing about semantics in classical logic in which it is possible to detect a contradiction or a tautology, while it is a problem to detect merely satisfiable formulas. I think what I really needed was a way to detect if the negation of `A -> B` that translates to `(A /\ ¬B)` is satisfiable, and the detection problem arose.
In classical logic, I think to derive `failure` from `(A /\ ¬B) -> failure` requires to explicitly state or derive both `A` and `¬B`. But if B does not follow from `A`, then `¬B` is not automatically concluded, thus `failure` doesn't get propagated.
So I decided to bend rules a bit, to match the last remark. I planned to make a system where if `B` does not follow from `A`, then `~B` is automatically concluded from `A` (or at least treated like so, not to bloat an output). In fact, in this system, if `X` is not a part of formula set, then `~X` automatically is. In this system, to prove that `B` doesn't follow from `A`, it would be enough to derive `~(A -> B)`. This completely changes raw logic semantics and it is not classical logic anymore.
However, classical not operation can still coexist in a form of `(¬X) = (X -> false)` statement, but now the negation `¬` is completely different operator than complementation `~`. The important thing is they should be able to both exist in the same system.
Last time I checked Martin Löf's type theory (a long time ago), it had an interesting property: sets are being inhabitated with proofs of their existence, while sets not being inhabitated at all are considered being false. This would somewhat correspond to a little system of mine, so finally, all of this might not be a completely new thing after all.
And then I found that the subject bugging me is already worked out:
autoepistemic logic,
negation as a failure, and
stable model semantics. Those are based on evidence, or a lack of evidence of some formula being true or false.
Of course, me wouldn't be me if I wasn't reinvent the hot water all by myself first. Why do I always have to do it the hard way?