https://scholars.lib.ntu.edu.tw/handle/123456789/315841
標題: | Refutational theorem proving using term-rewriting systems | 作者: | JIEH HSIANG | 公開日期: | 1985 | 卷: | 25 | 期: | 3 | 起(迄)頁: | 255-300 | 來源出版物: | Artificial Intelligence | 摘要: | In this paper we propose a new approach to theorem proving in first-order logic based on the term-rewriting method. First for propositional calculus, we introduce a canonical term-rewriting system for Boolean algebra. This system enables us to transform the first-order predicate calculus into a form of equational logic, and to develop several complete strategies (both clausal and nonclausal) for first-order theories based on the Knuth-Bendix Completion Procedure. More importantly, our strategies can deal with predicate logic and built-in (equational) theories in a uniform and effective way. We also describe an implementation and comparisons with some other first-order theorem-proving methods. © 1985. |
URI: | https://www.scopus.com/inward/record.uri?eid=2-s2.0-0022029327&doi=10.1016%2f0004-3702%2885%2990074-8&partnerID=40&md5=e6abd257e45f6b02855d2fcab5248ed4 http://scholars.lib.ntu.edu.tw/handle/123456789/315841 |
DOI: | 10.1016/0004-3702(85)90074-8 | SDG/關鍵字: | COMPUTER METATHEORY - Formal Logic; REFUTATIONAL THEOREM PROVING; TERM-REWRITING SYSTEMS; SYSTEMS SCIENCE AND CYBERNETICS |
顯示於: | 資訊工程學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。