Automated Support for Enterprise Information Systems

John Andrew Andrew van der Poll (University of South Africa, South Africa)

Paula Kotzé (University of South Africa, South Africa)

Willem Adrian Labuschagne (University of Otago, New Zealand)

Abstract: 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.

Keywords: OTTER, Z, automated reasoning, formal specification, heuristics, set theory

Categories: D.2.4, F.3.1, F.4.1, I.2.3