SATCHMORE: SATCHMO with RElevancy |
| |
Authors: | Donald W Loveland David W Reed Debra S Wilson |
| |
Affiliation: | (1) Department of Computer Science, Duke University, 27708 Durham, NC;(2) Present address: Department of Mathematics and Computer Science, Dickinson College, 17013 Carlisle, PA |
| |
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.This research was partially supported by NSF Grants IRI-8805696 and CCR-9116203. This paper is a major revision of Wilson and Loveland (1989). |
| |
Keywords: | SATCHMO relevancy detection Prolog theorem proving |
本文献已被 SpringerLink 等数据库收录! |
|