| I—SATCHMORE：An Improvement of A—SATCHMORE |
| |
| 引用本文： | 何立风.I—SATCHMORE：An Improvement of A—SATCHMORE[J].计算机科学技术学报,2003,18(2):181-189. |
| |
| 作者姓名： | 何立风 |
| |
| 作者单位： | [1]DepartmentofArtificialIntelligenceandComputerScience,NagoyaInstituteofTechnologyNagoya,466－8555Japan [2]FacultyofEnvironmentInformationandBusiness,NagoyaSangyoUniversity,Aichi,488－8711Japan [3]FacultyofInfo,NagoyaSangyoUniversity,Aichi,488－8711Japan |
| |
| 基金项目： | This research is partially supported by the Japan Society for the Promotion of Science. |
| |
| 摘 要： | This paper presents an improvement of A-SATCHMORE (SATCHMORE with Availability).A-SATCHMORE incorporates relevancy testing and availability checking into SATCHMO to prune away irrelevant forward chaining.However ,considering every consequent atom of those non-Horn clauses being derivable,A-SATCHMORE may suffer from a potential explosion of the search space when some of such consequent atoms are actually underivable.This paper introduces a solution for this problem and shows its correctness.
|
| 关 键 词： | 定理证明 可用性 前向连接 SATCHMORE |
<Emphasis Type="Italic">I</Emphasis>-SATCHMORE: An improvement of<Emphasis Type="Italic">A</Emphasis>-SATCHMORE |
| |
| LiFeng?HeEmail author,Chao?Yuyan,Nakamura?Tsuyoshi,Itoh?Hidenori.I-SATCHMORE: An improvement ofA-SATCHMORE[J].Journal of Computer Science and Technology,2003,18(2):181-189. |
| |
| Authors: | Email author" target="_blank">LiFeng?HeEmail author Chao?Yuyan Nakamura?Tsuyoshi Itoh?Hidenori |
| |
| Affiliation: | (1) Faculty of Information Science and Technology, Aichi Prefectural University, 480-1198 Aichi, Japan;(2) Faculty of Environment Information and Business, Nagoya Sangyo University, 488-8711 Aichi, Japan;(3) Department of Artificial Intelligence and Computer Science, Nagoya Institute of Technology, 466-8555 Nagoya, Japan |
| |
| Abstract: | This paper presents an improvement of A-SATCHMORE (SATCHMORE with Availability). A-SATCHMORE incorporates relevancy testing and availability checking into SATCHMO to prune away irrelevant forward chaining. However, considering every consequent atom of those non-Horn clauses being derivable, A-SATCHMORE may suffer from a potential explosion of the search space when some of such consequent atoms are actually underivable. This paper introduces a solution for this problem and shows its correctness. |
| |
| Keywords: | theorem proving availability forward chaining SATCHMO SATCHMORE A- SATCHMORE |
| 本文献已被 CNKI 维普 万方数据 SpringerLink 等数据库收录！ |
