Completeness of Hoare Logic Relative to the Standard Model

详细信息    查看全文

• 关键词：Hoare logic ; Peano arithmetic ; Arithmetical hierarchy ; The standard model ; Relative completeness
• 刊名：Lecture Notes in Computer Science
• 出版年：2017
• 出版时间：2017
• 年：2017
• 卷：10139
• 期：1
• 页码：119-131
• 丛书名：SOFSEM 2017: Theory and Practice of Computer Science
• ISBN：978-3-319-51963-0
• 卷排序：10139

文摘

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. This paper further studies the completeness of Hoare Logic relative to N with assertions restricted to subclasses of arithmetical formulas. Our completeness results refine Cook’s result by reducing the complexity of the assertion theory.