摘要：A condensed specification of a multi-level marketing (MLM) enterprise which can be modelled by mathematical forests and trees is presented in Z. We thereafter identify a number of proof obligations that result from operations on the state space. Z is based on first-order logic and a strongly-typed fragment of Zermelo-Fraenkel set theory, hence the feasibility of using certain reasoning heuristics developed for proving theorems in set theory is investigated for discharging the identified proof obligations. Using the automated reasoner OTTER, we illustrate how these proof obligations from a real-life enterprise may successfully be discharged using a suite of well-chosen heuristics.
关键词：OTTER, Z, automated reasoning, formal specification, heuristics, set theory
