The implementation works reasonably well. The functions of parsers, state monad
knowledge base, and the interactive system work great. One flaw is that instead
of composing monads in an elegant way in the file loading function (when IO
and state monads are used), a more ugly hack of
,
and
are used
and some of the hidden primitive functions in Prelude had to be copied over.
On the other hand, improvements can be made to the efficiency of the (CNF and
INF) normalization functions. In particular, checking for redundant literals
has not been implemented (i.e. reducing 
, 
,
, and
to 
).
The most difficult and quirky part of the project is the algorithm for making resolutions and proving using refutation. Presently, it is able to handle relatively simple set of knowledge bases. How well (or badly) it would perform when the knowledge base is big and the complexity of the proof is higer is questionable. Refining the efficiency of the algorithm and perhaps use a different approach (other than choosing the set-of-support strategy) could be the next imrovement.