The satisfiability of logical formula in proof of program
Cai Wang · Journal of Northwest Normal University · 2001
The satisfiability of logical formula and revelant algorithm in the program are discussed based on Herbrands theorem.The method on obtaining loop invariant of the given cyclic program is put forward.