Name
Abstract | ||
|---|---|---|
We present an improvement of SATCHMORE, calledA-SATCHMORE, by incorporating availability checking into relevancy. Because some atoms unavailable to the further computation
are also marked relevant, SATCHMORE suffers from a potential explosion of the search space. Addressing this weakness of SATCHMORE,
we show that an atom does not need to be marked relevant unless it is available to the further computation and no non-Horn
clause needs to be selected unless all its consequent atoms are marked availably relevant, i.e., unless it is totally availably
relevant. In this way,A-SATCHMORE is able to further restrict the ues of non-Horn clauses (therefore to reduce the search space) and makes the proof
more goal-oriented. Our theorem prover,A-SATCHMORE, can be simply implemented in PROLOG based on SATCHMORE. We discuss how to incorporate availability cheeking into
relevancy, describe our improvement and present the implementation. We also prove that our theorem prover is sound and complete,
and provide examples to show the power of our availability approach. |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1007/BF03037320 | New Generation Comput. |
Keywords | Field | DocType |
availability checking,search space,goal orientation,availability,theorem prover,theorem proving | Programming language,Computer science,Automated theorem proving,Theoretical computer science,Prolog,restrict,Computation | Journal |
Volume | Issue | ISSN |
16 | 1 | 0288-3635 |
Citations | PageRank | References |
7 | 0.55 | 4 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Lifeng He | 1 | 441 | 40.97 |
| Yuyan Chao | 2 | 315 | 24.07 |
| Yuka Shimajiri | 3 | 10 | 1.97 |
| Hirohisa Seki | 4 | 276 | 52.30 |
| Hidenori Itoh | 5 | 368 | 252.31 |