2017/03/01 by Zhaowei Xu, Wenhui Zhang, Xu, Zhaowei +3
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1703.00237
openalex publication_date 2017/03/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The general completeness problem of Hoare logic relative to the standard model N of Peano arithmetic has been studied by Cook, and it allows for the use of arbitrary arithmetical formulas as assertions. In practice, the assertions would be simple arithmetical formulas, e.g. of a low level in the arithmetical hierarchy. In addition, we find that, by restricting inputs to N, the complexity of the minimal assertion theory for the completeness of Hoare logic to hold can be reduced. This paper further studies the completeness of Hoare Logic relative to N by restricting assertions to subclasses of arithmetical formulas (and by restricting inputs to N). Our completeness results refine Cook's result by reducing the complexity of the assertion theory.