Institutional Repository
| Clausal presentation of theories in deduction modulo | |
| Gao, Jian-Hua (1); Gao, J.-H.(gaojh@ios.ac.cn) | |
| 2013 | |
| Source | Journal of Computer Science and Technology
 |
| ISSN | 10009000 |
| Volume | 28Issue:6Pages:1085-1096 |
| English Abstract | 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. |
| Indexed Type | SCI ; EI |
| Keyword | Resolution Deduction Modulo Cut Free Proof Clause |
| Department | (1) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China; (2) University of Chinese Academy of Sciences, Beijing 100049, China; (3) National Institute for Research in Computer Science and Control, Paris 78153, France |
| Language | 英语 |
| WOS ID | WOS:000326953200012 |
| Citation statistics | |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16905 |
| Collection | 中国科学院软件研究所 |
| Corresponding Author | Gao, J.-H.(gaojh@ios.ac.cn) |
| Recommended Citation GB/T 7714 | Gao, Jian-Hua ,Gao, J.-H.. Clausal presentation of theories in deduction modulo[J]. Journal of Computer Science and Technology,2013,28(6):1085-1096. |
| APA | Gao, Jian-Hua ,&Gao, J.-H..(2013).Clausal presentation of theories in deduction modulo.Journal of Computer Science and Technology,28(6),1085-1096. |
| MLA | Gao, Jian-Hua ,et al."Clausal presentation of theories in deduction modulo".Journal of Computer Science and Technology 28.6(2013):1085-1096. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment