An interpretation-oriented theorem prover over integersJames C. KingRobert W. Floyd1972Journal of Computer and System Sciences