dc.contributor.author |
Van der Poll, JA
|
|
dc.contributor.author |
Kotze, P
|
|
dc.contributor.editor |
Renaud, K.
|
|
dc.contributor.editor |
Kotze, P
|
|
dc.contributor.editor |
Barnard, A
|
|
dc.date.accessioned |
2018-08-23T11:32:18Z |
|
dc.date.available |
2018-08-23T11:32:18Z |
|
dc.date.issued |
2001 |
|
dc.identifier.citation |
Van der Poll, J.A. & Kotze, P. (2001) The specification of a multi-level marketing business. Hardware, Software and Peopleware: Proceedings of the Annual Conference of the South African Institute of Computer Scientists and Information Technologists, University of South Africa, Pretoria, 25-28 September 2001 |
en |
dc.identifier.isbn |
1-86888-195-4 |
|
dc.identifier.uri |
http://hdl.handle.net/10500/24778 |
|
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. Proof obligations aimed at corroborating the aptness of the specification are stated and discharged using the resolution-based, first-order theorem prover OTTER. Reasoning about two simple properties of the specification illustrates the utility of two automated reasoning strategies in the literature, namely avoiding equality and applying resonance. |
en |
dc.language.iso |
en |
en |
dc.subject |
Automated reasoning |
en |
dc.subject |
Formal specification |
en |
dc.subject |
Multi-level marketing |
en |
dc.subject |
OTTER |
en |
dc.subject |
Resolution |
en |
dc.subject |
Set theory |
en |
dc.subject |
Z |
en |
dc.title |
The specification of a multi-level marketing business |
en |