{\bf (Revision of CS-1994-16.)} SATCHMORE: SATCHMO with RElevancy
摘要
We introduce a relevancy detection algorithm to be used in conjunction with the SATCHMO prover. The version of SATCHMO considered here is essentially a bidirectional prover, utilizing Prolog (back chaining) on Horn clauses and forward chaining on non-Horn clauses. Our extension, SATCHMORE (SATCHMO with RElevancy), addresses the major weakness of SATCHMO: the uncontrolled use of forward chaining. By marking potentially relevant clause head literals, and then requiring that all the head literals be marked relevant (be ``totally relevant'''') before a clause is used for forward chaining, SATCHMORE is able to guide the use of these rules. Furthermore, the relevancy testing is performed without extending the proof search beyond what is done in SATCHMO. In addition, a very simple implementation of the extended SATCHMO can be written in Prolog. We describe our relevancy testing approach, present the implementation, prove soundness and completeness, and provide examples which demonstrate the power of relevancy testing.