Formalization of properties of recursively defined functions
Zohar Manna, Amir Pnueli · 1969
This paper is concerned with the relationship between the convergence, correctness and equivalence of recursively defined functions and the satisfiability (or unsatisfiability) of certain first-order formulas.