[Index] || [Contents] || [Grades] Tue Aug 5 11:44:58 PDT 2003

- DiscountsR'Us
- : Introduction
- : Situation
- : Exercises
- : Formal Analysis
- : Proof of completeness
- : Check
- : An Inconsistency
- : Fixing Requirements Creatively
- : Faster Methods
- : Links
- Index of defined terms etc.

- RULES::=following

Net- (R1): If a person has a club card and today is a Tuesday then the discount is 10%.
- (R2): If a person has a club card and today is not a Tuesday then the discount is 5%.
- (R3): If a person is a senior and has a club card then the discount is 10%.
- (R4): If a person is a senior and has not got a club card then the discount is 5%.
- (R5): If a person is not a senior and has not got a club card then the discount is 0%.

(End of Net RULES)

## Exercises

Exercise 1: Formalization. Invent a suitable abbreviation scheme and express these RULES in your scheme.

Exercise 2: Completeness. Prove that one of the RULES always applies. Note: If you have rules p->q then it applies when p is true. With rules p->q and r->s then one of them applies if (p \/ r) is true and so on...

Exercise 3. Inconsistency. Prove that if I have a club card and it is not Tuesday and I am a senior then the RULES mean I should get a 5% and a 10% discount.

Exercise 4. Creativity. Remove the inconsistency in exercise 3. Re-express the RULES. Prove completeness and consistency.

*. . . . . . . . . ( end of section Exercises)*<<Contents | Index>>## Formal Analysis

Abbreviations: (the '@' indicates a true/false proposition): - p::@, the person has a club card.
- q::@, today is Tuesday.
- r::@, the person is a senior.
- s::@, the discount is 10%.
- t::@, the discount is 5%.
- u::@, the discount is 0%.
Translating the

*RULES*into logical notation: - requirements::=following

Net

(End of Net)

A set of requirements is complete if every possibility has a defined response. So define

- completeness::= (p and q) or (p and not q) or (r and p) or (r and not p) or (not r and not p).
## Proof of completeness

- (LEM) |- (0): p or not p.

Let- (1): p
- (LEM) |- (2): q or not q

Let- (3): q
- (1, 3) |- p and q.
- (above) |-
*completeness*.

(Close Let q)

Let

(Close Let not q)

- (3): q
- (above, 2, ore) |-
*completeness*.

(Close Let p)

Let- (5): not p.
- (LEM) |- (6): r or not r.

Let

(Close Let r)

Let

(Close Let not r)

- (above, 6, ore) |-
*completeness*.

(Close Let not p)

- (1): p
- (above, 0, ore) |-
*completeness*.## Check

The above result can be checked semantically by evaluating every possible combination of true and false for p, q, r. Here is a link to a Prolog program that helps do this: [ discounts.plg ]## An Inconsistency

Prove: if (p and not q and r ) then (s and t).

Let- (9): p and not q and r.
- (9) |- (10): p and not q,
- (10, r2) |- (11): t.
- (10) |- (12): p.
- (9) |- (13): r.
- (12, 13) |- (14): r and p.
- (14, r3) |- (15): s.
- (11, 15) |- (16): s and t.

(Close Let )

## Fixing Requirements Creatively

There are many ways of resolving the above inconsistency. For example give a 15% discount to a senior with a club card. Formalizing and checking the new requirements is time consuming but essential.## Faster Methods

Proofs are not the fastest way to check the requirements in this document. If there are less than 5 propositions in the conditions then a Karnaugh Map can be used to plot the different conclusions. Parnas's function tables expose problems well and make the requirements clearer. And/Or tables are simple and easy to read but they are best analyses by a tool. For more see*TABLES*below. For more complex requirements expressed in the Propositional Calculus a tool is a great help.## Links

- (9): p and not q and r.
- above::=
*results proved above this one*. - logic::= See http://www.csci.csusb.edu/dick/cs656/logic.html.
- LEM::= See http://www.csci.csusb.edu/dick/cs656/logic.html#LEM.
See
*HuthRyan00*page 28. - ore::= See http://www.csci.csusb.edu/dick/cs656/logic.html#ore.
See
*HuthRyan00*page 19. - ori::= See http://www.csci.csusb.edu/dick/cs656/logic.html#ori.
See
*HuthRyan00*page 19. - TABLES::= See http://www.csci.csusb.edu/dick/cs656/tables.pdf
- HuthRyan00::=
*text book for CSci656/556, Logic in Computer Science*.*. . . . . . . . . ( end of section DiscountsR'Us)*<<Contents | Index>>

- 0 (Theorem)
- 10 (Theorem)
- 11 (Theorem)
- 1 (Label)
- 12 (Theorem)
- 13 (Theorem)
- 14 (Theorem)
- 15 (Theorem)
- 16 (Theorem)
- 2 (Theorem)
- 3 (Label)
- 4 (Label)
- 5 (Label)
- 6 (Theorem)
- 7 (Label)
- 8 (Label)
- 9 (Label)
- above (Definition)
- completeness (Definition)
- HuthRyan00 (Definition)
- LEM (Definition)
- logic (Definition)
- ore (Definition)
- ori (Definition)
- p (Declaration)
- q (Declaration)
- R1 (Formula)
- r1 (Label)
- R2 (Formula)
- r2 (Label)
- R3 (Formula)
- r3 (Label)
- R4 (Formula)
- r4 (Label)
- R5 (Formula)
- r5 (Label)
- requirements (Definition)
- r (Declaration)
- RULES (Definition)
- s (Declaration)
- TABLES (Definition)
- t (Declaration)
- u (Declaration)