RESOLVE (REusable SOftware Language with VErification) is a specification and programming language designed for verifying correctness of object oriented programs.
Rather than producing x /= y when negating the expression x = y, we now produce not(x = y). The reason we do this is so that the sequent reduction rules can take care of it.
Rather than producing
x /= ywhen negating the expressionx = y, we now producenot(x = y). The reason we do this is so that the sequent reduction rules can take care of it.