i happen to have a theoretical question about input resolution in logic.
so in input resolution we can use the resolution rule/theorem if at least one out of two clauses in the resolution are from the from the original proposition.
now my question is this: is the input resolution complete to contradiction?
i mean, If you take a claim(proposition) that is a result from the knowledge base and add its contradiction(negation) to the knowledge base, then can we deduct an empty proposition(contradiction) using the inference rules?
would really interested in learning from your inputs. really curious