An Improvement on Sub-Herbrand Universe Computation

Lifeng He1, *, , Yuyan Chao2, *, , Kenji Suzuki3, Zhenghao Shi 3, Hidenori Itoh 4
Graduate School of Information Science, Aichi Prefectural University, Aichi, Japan
Graduate School of Environment Management, Nagoya Sangyo University, Aichi, Japan
Department of Radiology, The University of Chicago, Chicago, IL, USA
Department of Information, Nagoya Institute of Technology, Nagoya, Japan

© 2017 He et al.;

open-access license: This is an open access article distributed under the terms of the Creative Commons Attribution 4.0 International Public License (CC-BY 4.0), a copy of which is available at: ( This license permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.

* *Address correspondence to this author at the Graduate School of Information Science, Aichi Prefectural University, Nagakute-cho, Aichi-gun, Aichi 480-1198, Japan; Tel: +81-561-64-1111, Ext. 3311; Fax: +81-561-64-1108; E-mail:
Also with Shannxi University of Science and Technology, Xianyang, Shannxi, China.


This paper presents an efficient algorithm for computing sub-Herbrand universes for arguments of functions and predicates in a given clause set. Unlike the previous algorithm, which processes all clauses in the given clause set once for computing each sub-Herbrand universe, the proposed algorithm computes all sub-Herbrand universes in the clause set by processing each clause in the clause set only once. We prove the correctness of our algorithm, and we provide experimental results on theorem proving benchmark problems to show the power of our approach.