A multi-level Marketing case study : specifying forests and trees in Z

dc.contributor.author	Van der Poll, J.A.
dc.contributor.author	Kotze, P.
dc.date.accessioned	2012-01-30T11:33:00Z
dc.date.available	2012-01-30T11:33:00Z
dc.date.issued	2003-06
dc.identifier.uri	http://hdl.handle.net/10500/5293
dc.description.abstract	A formal specification of a multi-level marketing (MLM) business is presented. Specifying a MLM business boils down to specifying properties of and operations on mathematical forests and trees. The usefulness of the model-based specification language, Z, is investigated as a vehicle for a formal specification of these recursive structures. The specification is presented following a prescribed format, namely the Established Strategy for constructing a Z specification. The Established Strategy is augmented with the notion of proof aimed at corroborating the correctness of critical parts of a specification. We show how attempts at discharging two different proof obligations using the resolution-based, first-order theorem prover OTTER calls for the use of two automated reasoning strategies, namely avoiding equality and using resonance.	en
dc.language.iso	en	en
dc.subject	Automated reasoning	en
dc.subject	Established Strategy	en
dc.subject	Formal specification	en
dc.subject	Multi-level marketing	en
dc.subject	OTTER	en
dc.subject	Precondition calculation	en
dc.subject	Resolution	en
dc.subject	Schema	en
dc.title	A multi-level Marketing case study : specifying forests and trees in Z	en
dc.type	Article	en