PROOF OF UNSATISFIABILITY OF ATOM SETS BASED ON COMPUTATION BY EQUIVALENT TRANSFORMATION RULES

Equivalent Transformation (ET) rules can be used to construct correct sequential and parallel programs, as they are inherently correct. One important method for making ET rules uses logical formulas. Among logical formulas, unsatisfiable conjunctions of finite atoms, each of which is represented by an atom set in this paper, are especially useful for making many ET rules that are used for constructing efficient programs. This paper proposes a method of proving unsatisfiability of an atom set based on computation by ET rules. The proposed method is recursive, in the sense that, during proving the given atom set, it may find a new atom set based on subset relation or inductive structure. Since our proposed method incorporates search based on subset and inductive relations, it can be used to prove unsatisfiability of various atom sets that cannot be proven by conventional methods