I need to implement resolution refutation for predicate logic to verify if a set of clauses form a logical consequence of a given set of antecedent clauses. I need to code this in SML. Can someone help me to get started ?? Thanks and Regards.
Implementation Of Resolution Refutation In SML
1
$\begingroup$
logic
propositional-calculus