Linear strategy for boolean ring based theorem proving |
| |
Authors: | Jinzhao Wu Zhuojun Liu |
| |
Affiliation: | (1) Max-Planck-Institut für Informatik, Im Stadtwald, 66123 Saarbrücken, Germany;(2) Institute of Systems Science, Chinese Academy of Sciences, 100080 Beijing, P.R. China |
| |
Abstract: | Two inference rules are discussed in boolean ring based theorem proving, and linear strategy is developed. It is shown that both of them are complete for linear strategy. Moreover, by introducing a partial ordering on atoms, pseudo O-linear and O-linear strategies are presented. The former is complete, the latter,however, is complete for clausal theorem proving. |
| |
Keywords: | Boolean ring linear strategy Herbrand theorem O-linear strategy |
本文献已被 CNKI 维普 万方数据 SpringerLink 等数据库收录! |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载免费的PDF全文 |
|