An interpretation-oriented theorem prover over integers
作者：
Highlights：
•
摘要
A special purpose theorem prover for establishing the validity of expressions over integer variables was developed as part of a program verifier. It is built around a powerful system for manipulating and simplifying integer expressions.
论文关键词：
论文评审过程：Received 15 December 1971, Available online 27 December 2007.
论文官网地址：https://doi.org/10.1016/S0022-0000(72)80024-2
