Clausal presentation of theories in deduction modulo
文献类型：期刊论文
| 作者 | Gao, Jian-Hua (1) |
| 刊名 | Journal of Computer Science and Technology
 |
| 出版日期 | 2013 |
| 卷号 | 28期号:6页码:1085-1096 |
| 关键词 | resolution deduction modulo cut free proof clause |
| ISSN号 | 10009000 |
| 通讯作者 | Gao, J.-H.(gaojh@ios.ac.cn) |
| 中文摘要 | Resolution modulo is an extension of first-order resolution in which rewrite rules are used to rewrite clauses during the search. In the first version of this method, clauses are rewritten to arbitrary propositions. These propositions are needed to be dynamically transformed into clauses. This unpleasant feature can be eliminated when the rewrite system is clausal, i.e., when it rewrites clauses to clauses. We show in this paper how to transform any rewrite system into a clausal one, preserving the existence of cut free proofs of any sequent. © 2013 Springer Science+Business Media New York & Science Press, China. |
| 英文摘要 | Resolution modulo is an extension of first-order resolution in which rewrite rules are used to rewrite clauses during the search. In the first version of this method, clauses are rewritten to arbitrary propositions. These propositions are needed to be dynamically transformed into clauses. This unpleasant feature can be eliminated when the rewrite system is clausal, i.e., when it rewrites clauses to clauses. We show in this paper how to transform any rewrite system into a clausal one, preserving the existence of cut free proofs of any sequent. © 2013 Springer Science+Business Media New York & Science Press, China. |
| 收录类别 | SCI ; EI |
| 语种 | 英语 |
| WOS记录号 | WOS:000326953200012 |
| 公开日期 | 2014-12-16 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/16905]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文 |
| 推荐引用方式 GB/T 7714 | Gao, Jian-Hua . Clausal presentation of theories in deduction modulo[J]. Journal of Computer Science and Technology,2013,28(6):1085-1096. |
| APA | Gao, Jian-Hua .(2013).Clausal presentation of theories in deduction modulo.Journal of Computer Science and Technology,28(6),1085-1096. |
| MLA | Gao, Jian-Hua ."Clausal presentation of theories in deduction modulo".Journal of Computer Science and Technology 28.6(2013):1085-1096. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。