resolution refutation is method of finding whether the given antecedent implies the consequent or not, it could also be used to check validity of the expressions.
Resolution refutation method is just refutation complete.
You need a prolog interpreter to be installed on your system.
preferably, swipl as the given files are tested against swipl-prolog-interpreter only.
If you are using swipl interpreter, execute swipl
and then write
? [resolution]. <press Enter>
? start. <press Enter>
to get the instructions.
For the better understanding of the process going on durng execution and to understand how the antecedents and consequents are getting processed, uncomment all the comments in the program, you can easily do this by using find and replace, and then re-execute.