RESEARCH ARTICLE
An Improvement on Sub-Herbrand Universe Computation
Lifeng He1, *, †, Yuyan Chao2, *, †, Kenji Suzuki3, Zhenghao Shi 3, Hidenori Itoh 4
Article Information
Identifiers and Pagination:
Year: 2007Volume: 1
First Page: 12
Last Page: 18
Publisher Id: TOAIJ-1-12
DOI: 10.2174/1874061800701010012
Article History:
Electronic publication date: 26/11/2007Collection year: 2007
© 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: (https://creativecommons.org/licenses/by/4.0/legalcode). This license permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.
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: (https://creativecommons.org/licenses/by/4.0/legalcode). This license permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.
Abstract
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.