期刊文献+
共找到1篇文章
< 1 >
每页显示 20 50 100
An Improvement of Herbrand's Theorem and Its Application to Model Generation Theorem Proving
1
作者 Yu-Yan Chao Li-Feng He +3 位作者 Tsuyoshi Zheng-Hao Shi Kenji Suzuki Hidenori Itoh 《Journal of Computer Science & Technology》 SCIE EI CSCD 2007年第4期541-553,共13页
This paper presents an improvement of Herbrand's theorem.We propose a method for specifying a subuniverse of the Herbrand universe of a clause set S for each argument of predicate symbols and function symbols in S... This paper presents an improvement of Herbrand's theorem.We propose a method for specifying a subuniverse 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. 展开更多
关键词 Herbrand's theorem Herbrand universe model generation theorem proving SATCHMO really non-propositional
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部