1
$\begingroup$

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.

$\endgroup$

1 Answer 1

1
$\begingroup$

Larry Paulson is best known as pioneer and grand master of theorem prover implementation in SML in the 1980-ies and 1990-ies. His classic text book "ML for the Working Programmer" has a tactical prover in chapter 10 as full worked example. You can get the ML sources from ML book without buying the book.

This assumes an educational background for this question. If you want a real system you should take Isabelle from today (2013).

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .