Z-SATCHMORE: An Improvement of A-SATCHMORE

This paper presents an improvement of A-SATCHMORE (SATCHMOREwith Availability). A-SATCHMORE incorporates relevancy testingand availability checking into SATCHMO to prune away irrelevant forwardchaining. However, considering every consequent atom of those non-Hornclauses being derivable, A-SATCHMORE may suffer from apotential explosion of the search space when some of such consequentatoms are actually underivable. This paper introduces a solution forthis problem and shows its correctness.