| An Improvement of Herbrands Theorem and Its Application to Model Generation Theorem Proving |
| |
| 作者姓名： | Yu-Yan Chao Li-Feng He Tsuyoshi Nakamura Zheng-Hao Shi Kenji Suzuki and Hidenori Itoh |
| |
| 作者单位： | Graduate School of Environment Management Nagoya Sangyo University，Aichi，Japan College of Mechanical and Electrical Engineering，Shaanxi University of Science and Technology，China，Graduate School of Information Science and Technology，Aichi Prefectural University，Aichi，Japan College of Computer and Information Engineering，Shaanxi University of Science and Technology，China，Gurrently，Research Associate，The University of Chicago，USA.，Graduate School of Computer Science and Engineering，Nagoya Institute of Technology，Nagoya，Japan，Graduate School of Computer Science and Engineering，Nagoya Institute of Technology，Nagoya，Japan，Department of Radiology，The University of Chicago，Chicago，U.S.A.，Graduate School of Computer Science and Engineering，Nagoya Institute of Technology，Nagoya，Japan |
| |
| 基金项目： | This work was supported partially by TOYOAKI Scholarship Foundation,Japan. |
| |
| 摘 要： | This paper presents an improvement of Herbrand's theorem.We propose a method for specifying a sub- universe of the Herbrand universe of a clause set S for each argument of predicate symbols and function symbols in S. We prove that a clause set S is unsatisfiable if and only if there is a finite unsatisfiable set of ground instances of clauses of S that are derived by only instantiating each variable,which appears as an argument of predicate symbols or function symbols,in S over its corresponding argument's sub-universe of the Herbrand universe of S.Because such sub-universes are usually smaller(sometimes considerably)than the Herbrand universe of S,the number of ground instances may decrease considerably in many cases.We present an algorithm for automatically deriving the sub-universes for arguments in a given clause set,and show the correctness of our improvement.Moreover,we introduce an application of our approach to model generation theorem proving for non-range-restricted problems,show the range-restriction transformation algorithm based on our improvement and provide examples on benchmark problems to demonstrate the power of our approach.
|
| 收稿时间： | 21 June 2006 |
An Improvement of Herbrand's Theorem and Its Application to Model Generation Theorem Proving |
| |
| Yu-Yan Chao,Li-Feng He,Tsuyoshi Nakamura,Zheng-Hao Shi,Kenji Suzuki,and Hidenori Itoh.An Improvement of Herbrands Theorem and Its Application to Model Generation Theorem Proving[J].Journal of Computer Science and Technology,2007,22(4):541-553. |
| |
| Authors: | Yu-Yan Chao Li-Feng He Wsuyoshi Nakamura Zheng-Hao Shi Kenji Suzuki Hidenori Itoh |
| |
| Affiliation: | (1) Graduate School of Environment Management, Nagoya Sangyo University, Aichi, Japan;(2) College of Mechanical and Electrical Engineering, Shaanxi University of Science and Technology, Shaanxi, China;(3) Graduate School of Information Science and Technology, Aichi Prefectural University, Aichi, Japan;(4) College of Computer and Information Engineering, Shaanxi University of Science and Technology, Shaanxi, China;(5) Graduate School of Computer Science and Engineering, Nagoya Institute of Technology, Nagoya, Japan;(6) Department of Radiology, The University of Chicago, Chicago, USA;(7) Currently, Research Associate, The University of Chicago, Chicago, USA |
| |
| Abstract: | This paper presents an improvement of Herbrand's theorem.We propose a method for specifying a sub- universe of the Herbrand universe of a clause set S for each argument of predicate symbols and function symbols in S. We prove that a clause set S is unsatisfiable if and only if there is a finite unsatisfiable set of ground instances of clauses of S that are derived by only instantiating each variable,which appears as an argument of predicate symbols or function symbols,in S over its corresponding argument's sub-universe of the Herbrand universe of S.Because such sub-universes are usually smaller(sometimes considerably)than the Herbrand universe of S,the number of ground instances may decrease considerably in many cases.We present an algorithm for automatically deriving the sub-universes for arguments in a given clause set,and show the correctness of our improvement.Moreover,we introduce an application of our approach to model generation theorem proving for non-range-restricted problems,show the range-restriction transformation algorithm based on our improvement and provide examples on benchmark problems to demonstrate the power of our approach. |
| |
| Keywords: | Herbrand's theorem Herbrand universe model generation theorem proving SATCHMO really non-propositional |
| 本文献已被 CNKI 万方数据 SpringerLink 等数据库收录！ |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载全文 |
|
