Evaluating reasoning heuristics in the context of multi-level marketing structures
John Andrew van der Poll, Paula Kotzé · South African Institute of Computer Scientists and Information Technologists · 2004
A reduced specification of a multi-level marketing business modelled by mathematical forests and trees is presented in the Z specification language. A number of proof obligations arising from operations on the state is identified. Since Z is based on first-order logic and a strongly typed fragment of Zermelo-Fraenkel set theory, the utility of a number of heuristics for reasoning about set-theoretic constructs is investigated to discharge the identified proof obligations. Using the resolution-based theorem-proving program OTTER, we illustrate how these proof obligations may successfully be discharged using a set of well-chosen heuristics.