[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> discounts
[Index] || [Contents] || [Grades] Tue Aug 5 11:44:58 PDT 2003

Contents

    DiscountsR'Us

    Introduction

     The following example shows how conflicting requirements arise and how they can be recognized by using logic. In this case semantic techniques ( [ Faster Methods ] below) work best. However, the same scenario can be tackled by using Natural Deduction.

    Situation

    A certain store has complicated scheme for calculating discounts that we are programming into the store's computerized point of sale terminals. Here are the rules:
  1. RULES::=following
    Net
    1. (R1): If a person has a club card and today is a Tuesday then the discount is 10%.
    2. (R2): If a person has a club card and today is not a Tuesday then the discount is 5%.
    3. (R3): If a person is a senior and has a club card then the discount is 10%.
    4. (R4): If a person is a senior and has not got a club card then the discount is 5%.
    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):
  2. p::@, the person has a club card.
  3. q::@, today is Tuesday.
  4. r::@, the person is a senior.
  5. s::@, the discount is 10%.
  6. t::@, the discount is 5%.
  7. u::@, the discount is 0%.

    Translating the RULES into logical notation:

  8. requirements::=following
    Net

      (r1): if p and q then s
      (r2): if p and not q then t
      (r3): if r and p then s
      (r4): if r and not p then t
      (r5): if not r and not p then u

    (End of Net)

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

  9. 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


  10. (LEM) |- (0): p or not p.
    Let
    1. (1): p
    2. (LEM) |- (2): q or not q
      Let
      1. (3): q
      2. (1, 3) |- p and q.
      3. (above) |- completeness.

      (Close Let q)

      Let
      1. (4): not q
      2. (1, 4) |- p and not q.
      3. (above, ori) |- completeness.

      (Close Let not q)

    3. (above, 2, ore) |- completeness.

    (Close Let p)

    Let
    1. (5): not p.


    2. (LEM) |- (6): r or not r.
      Let
      1. (7): r.
      2. (5, 7) |- not p and r,
      3. (above, ori) |- completeness

      (Close Let r)

      Let
      1. (8): not r
      2. (5, 8) |- not p and not r,
      3. (above, ori) |- completeness

      (Close Let not r)


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

    (Close Let not p)

  11. (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
    1. (9): p and not q and r.
    2. (9) |- (10): p and not q,
    3. (10, r2) |- (11): t.


    4. (10) |- (12): p.
    5. (9) |- (13): r.
    6. (12, 13) |- (14): r and p.
    7. (14, r3) |- (15): s.
    8. (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

  12. above::=results proved above this one.
  13. logic::= See http://www.csci.csusb.edu/dick/cs656/logic.html.
  14. LEM::= See http://www.csci.csusb.edu/dick/cs656/logic.html#LEM. See HuthRyan00 page 28.
  15. ore::= See http://www.csci.csusb.edu/dick/cs656/logic.html#ore. See HuthRyan00 page 19.
  16. ori::= See http://www.csci.csusb.edu/dick/cs656/logic.html#ori. See HuthRyan00 page 19.
  17. TABLES::= See http://www.csci.csusb.edu/dick/cs656/tables.pdf
  18. HuthRyan00::=text book for CSci656/556, Logic in Computer Science.

    . . . . . . . . . ( end of section DiscountsR'Us) <<Contents | Index>>

Formulae and Definitions in Alphabetical Order