ISSN:
1573-0670
Keywords:
SATCHMO
;
relevancy detection
;
Prolog
;
theorem proving
;
68T15
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract 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. A 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 that demonstrate the power of relevancy testing.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00881861
Permalink
