JUCS - Journal of Universal Computer Science 10(11): 1519-1539, doi: 10.3217/jucs-010-11-1519
Automated Support for Enterprise Information Systems
expand article infoJohn Andrew Andrew Van Der Poll‡, Paula Kotzé‡, Willem Adrian Labuschagne§
‡ University of South Africa, South Africa§ University of Otago, New Zealand

Corresponding author: John Andrew Andrew Van Der Poll ( vdpolja@unisa.ac.za )

© John Andrew Andrew Van Der Poll, Paula Kotzé, Willem Labuschagne.
This article is freely available under the J.UCS Open Content License.
Citation: Van Der Poll JAA, Kotzé P, Labuschagne WA (2004) Automated Support for Enterprise Information Systems. JUCS - Journal of Universal Computer Science 10(11): 1519-1539. https://doi.org/10.3217/jucs-010-11-1519
Open Access
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
automated reasoning, formal specification, heuristics, OTTER, set theory, Z