Conclude that some cats which are in love are hungry. We want to know whether the conclusion is logically justified or not. It is easy to see that any reasonable resolution refinement terminates on C, without inferring the empty clause. There are arbitrarily many possibilities to modify a statement so that it becomes valid. No hungry cat gazes at the moon.
Some cats gazing at the moon are in love.
We denote the corresponding formula as F'. Applying resolution to the new clause set C', sat-equivalent to not F', we derive the empty clause. Hence, the new conclusion is justified. We call this approach to Automated Model building resolution-based . The deduction system TILT implements the recent results of the Vienna Group.