The correctness of nondeterministic programs

摘要

In this paper we formalize properties of nondeterministic programs by means of the satisfiability and validity of formulas in first-order logic. Our main purpose is to emphasize the great variety of possible applications of the results, especially for solving problems of the kind: “Find a sequence of actions that will achieve a given goal.”