exam in discrete math
A1Homework_01
FrmlMeth.SoftwareEXLSGroupCASpringSemester2018CO-4262018-740AM.zipOverview.html
This unit will teach how to use propositional calculus to simplify and reason about statements of requirements.
Learning Objectives: Related course level objectives: 2 and 3
After completing the tasks of Module 6:
1. The student will be able to use propositional calculus to construct proofs to show whether or not a conclusion follows from a set of premises.
2. The student will be able to express a system specification written in natural language in propositional calculus, and construct proofs using propositional calculus to analyze and reason about the system specification.
Tasks: To achieve the learning objectives of this module, you must do the following:
Read sections 3.4, 3.5 in Ince.
Read all the notes included in the section
Do the homework assignment on section 3.5
Participate and lead (start threads and reply to threads) the discussion on Requirements and Propositional Calculus-Section 3.4 in the Content Forum of the Discussion Tool.
note_for_indirect_proofV2.doc
3.4.2 Reasoning
Indirect Proof or Proof by Contradiction
Example:
To demonstrate
¬ ChannelOpen ├ sender
ChannelOpen V sender is known from the system specification.
Recall that any statement that is given or derived is assumed to be TRUE.
[pr1] ¬ sender ( assume conclusion is false
[pr2] ¬ ChannelOpen ***this is true
[pr3] ChannelOpen V sender *** and this is true
Since we know from p2 that ¬ ChannelOpen is TRUE, then we know ChannelOpen must be false. So using =commV we can change pr3 to [1] and using =or3 we get:
[1] sender V ChannelOpen [pr3, =commV]
[2] sender V false [1, pr2, defn ¬]
[3] sender [ 2, =or 3 ]
Putting 3 and pr1 together via =AND5 we get:
[4] sender Λ ¬ sender [ pr1, 3, = and 5 ]
[5] false [ 4, = contr ]
So what does this mean? To prove
¬ ChannelOpen ├ sender
using indirect proof, we assumed the premises are all true and the conclusion is false. If this leads to a contradiction, it proves the conclusion CAN be deduced from the premises.
For Section 3.6 You are going to need to use implies and impliesnot for these problems.
Worked Example 3.9
Demonstrate: open => normal ├ normal V ShutDown
S1: closed => ShutDown
S2: open V closed
[pr1] ¬ (normal V ShutDown) ( assume conclusion is false
[pr2] open => normal
[pr3] closed => ShutDown
[pr4] open V closed
[1] ¬ normal Λ ¬ ShutDown [ pr1, = DeM V ]
***So if a Λ b are true, we can separate them and each is true using =and5.
[2] ¬ normal [ 1, = and 5 ]
[3] ¬ ShutDown [ 1, = and 5 ]
***We’re looking for a contradiction, so what do we know? Combine pr2 and 2:
[4] ¬ open [ pr2, 2, impliesnot ]
***We’re looking for a contradiction, so what else do we know? Combine pr3 and 3:
[5] ¬ closed [ pr3, 3, impliesnot ]
***We’re looking for a contradiction, so what can we put together? Combine 4 and 5 using =and5:
[6] ¬ open Λ ¬ closed [4, 5, = and 5 ]
***Make it more “user-friendly” with DeMorgan’s:
[7] ¬ (open V closed) [6, = DeM V ]
***Put pr4 together with 7 using =and5 gives [pr3]
[8] (open V closed) Λ ¬ (open V closed) [7, pr4, =and5]
[9] false [ 8, = contr ]
***Since we found a contradiction, we have proved what we wanted to prove: we demonstrated that the conclusion follows from the premises.
Next Example
Demonstrate: scheduler ├ ¬ FirstFit
With S1: scheduler => FirstFit V BestFit
[pr1] FirstFit ( assume conclusion is false
[pr2] scheduler
[pr3] scheduler => FirstFit V BestFit
***So what do we know? Using implies we know:
[1] FirstFit V BestFit [pr2,pr3, implies ]
***What else can we show? Use =impl to manipulate pr3:
[2] ¬ scheduler V (FirstFit V BestFit) [ pr3, = impl ]
*** We can’t separate an OR statement like we do with AND, so what else? Since by [1] we know FirstFit V BestFit is true, we have in [2]: ¬ scheduler V true, which is:
[3] true / no contradiction [ 2, =or2 ]
Therefore, since we cannot generate a contradiction, it follows that the conclusion cannot be deduced from the premises.
Worked Example 3.10
Demonstrate: normal => printing ├ ¬LpAvailable
S1: LpAvailable V spooler => normal V online
S2: ¬ printing
[pr1] LpAvailable ( assume conclusion is false
[pr2] normal => printing
[pr3] LpAvailable V spooler => normal V online
[pr4] ¬ printing
***What do we know? Let’s use impliesnot:
[1] ¬normal [pr2, pr4, impliesnot]
***Can we build something using or5 that might help?
[2] LpAvailable V spooler [pr1, or5]
***Combine 2 and pr3:
[3] normal V online [2, pr3, implies]
***Change it around:
[4] online V normal [3, commV]
***Now since we know ¬normal is true, then normal is false so we have online V false
[5] online [4, =or3]
***Now what? We’ve used all the premises and didn’t get a contradiction so:
[6] no contradiction
Therefore, since we cannot generate a contradiction, it follows that the conclusion cannot be deduced from the premises.
formal_methods_notes for Sect3.5.docx
Simplifying System Specifications --Examples
Consider the statement below taken from a system specification:
“If the valve is opened, then the inlet controller is placed in a monitoring state, if the system is not in a startup mode.”
Represent the above in propositional calculus:
ValveOpened => (¬ startup => monitoring)
Now simplify using =impl
¬ ValveOpened V (¬ startup => monitoring)
Simplify again using = impl:
¬ ValveOpened V startup V monitoring
¬ ValveOpened V startup V monitoring
This represents:
“Either the valve is not opened or the system is in a startup mode or the inlet controller is in a monitoring state.”
Assume a later proposition in the specification states:
“The valve is opened and the system is not in startup mode and the inlet controller is not in a monitoring state.”
In propositional calculus:
(2) ValveOpened Λ ¬ startup Λ ¬ monitoring
But this contradicts the earlier expression
(1) ¬ ValveOpened V startup V monitoring
How?
Assuming (1) is TRUE, for what values of the variables is (2) TRUE?
Example: Express in propositional calculus and derive the relationships between the monitoring state, the test state, and the fact that the reactor is operating.
“The reactor is either in the monitoring or test state. It cannot be in both states. The reactor is functioning normally only when it is in one of these states.”
“If a reactor is functioning normally and is not in the test state then the reactor can be regarded as being operating.”
Normal monitoring Ve test
And
Normal Λ ¬test => operating
[p1] normal monitoring Ve test
[p2] normal Λ ¬ test => operating
[1] normal (monitoring Λ ¬ test) V (¬ monitoring Λ test) [P1, = Exor]
[2] (monitoring Λ ¬ test) V ( ¬ monitoring Λ test) Λ
¬ test => operating [p2, 1, Subst (rt side of 1 into “normal” in p2)]
[2a] (monitoring Λ ¬ test) V (( ¬ monitoring Λ test) Λ
¬ test) => operating [2, order of operations]
[2b] (monitoring Λ ¬ test) V ( ¬ monitoring Λ test Λ
¬ test) => operating [2a, =lassocΛ]
[3] (monitoring Λ ¬ test) V ( ¬ monitoring Λ (test Λ
¬ test)) => operating [2b, =rassocΛ]
[4] (monitoring Λ ¬ test) V (¬ monitoring Λ false) => operating [3, =contr]
[5] (monitoring Λ ¬test) V false => operating [4, =and3]
[5a] false V (monitoring Λ ¬test) => operating
[5, =commV]
[5b] (false V monitoring) Λ (false V ¬test) => operating
[5a, =dist VΛ]
[5c] (monitoring V false) Λ (false V ¬test) => operating
[5b, =comm V]
[5d] monitoring Λ (false V ¬test) => operating [5c, =or3]
[5e] monitoring Λ (¬test V false) => operating [5d, =commV]
[6] monitoring Λ ¬test => operating [5e,=or3]
You could use =impl but above is probably simplest form.
(NOTE 6 steps in the book become 13 if you do one operation at a time.) Example: During requirements analysis and design questions arise like:
“If the reactor is in the steady state and an update command is typed, does that mean that the reactor no longer remains in the steady state”
Premises taken from the question above:
Reactor is in a steady state,
Update command is typed.
And the conclusion:
Reactor is not in a steady state.
Example:
The fact that a conclusion ValveOpen follows from the premises NormalState, OpenCommand , and ¬ TestState can be written as:
NormalState, OpenCommand, ¬ TestState |─ ValveOpen
It represents the question: “ Would the valve be open if the reactor is in its normal state and the open command has been typed and the reactor is not in a test state”?
Premises and conclusions can be simple proposition as above or can be formed from existing propositions and the propositional operators.
Example: Show the conclusion follows from the premises.
¬ closed, open V closed |─ open
Rewritten as:
¬ closed Λ (open V closed) => open
[pr] ¬ closed Λ (open V closed) => open
[1] ¬(¬ closed Λ (open V closed)) V open [pr, = impl]
[2]¬ ¬ closed V ¬ (open V closed) V open [1, = DeMΛ]
[3] closed V ¬ (open V closed) V open [2, = neg]
[4] closed V open V ¬ (open V closed) [3, = commV]
[5] (closed V open) V ¬ (closed V open) [4,= commV, =lassocV]
[6] true [5, = exmid]
It is a tautology and the conclusion logically follows.
Example: Show that the conclusion ¬ LineClosed follows from the premises
ChannelOpen, ReceiverReady,
LineClosed Λ ChannelOpen => ¬ ReceiverReady
Solution: We need to show:
ChannelOpen Λ ReceiverReady Λ (LineClosed Λ ChannelOpen => ¬ ReceiverReady) => ¬ LineClosed
First start simplifying the propositional expression to the left of the implication.
Before you look at this, let me tell you this is probably the hardest, and definitely the longest, problem in the book. Read through your author’s explanation before going through this next problem and see if his solution makes any sense to you. I attacked it with a hammer – one step at a time – which is sometimes difficult to do.
[pr] [ChannelOpen Λ ReceiverReady Λ (LineClosed Λ ChannelOpen =>
¬ ReceiverReady)] => ¬ LineClosed
To make this easier to read,
Let CO= ChannelOpen, RR= ReceiverReady, LC =LineClosed
[pr] [CO Λ RR Λ (LC Λ CO => ¬RR)] => ¬LC
[1] [CO Λ RR Λ (¬ (LC Λ CO) V ¬ RR)] => ¬ LC [pr, = impl]
[2] [CO Λ RR Λ (¬ LC V ¬ CO V ¬ RR)] => ¬ LC [1, = DeM Λ ]
[2a] [CO Λ RR Λ ((¬ LC V ¬ CO) V ¬ RR)] => ¬ LC [2, = lassoc V]
[2b] [CO Λ RR Λ (¬ RR V (¬LC V ¬ CO))] => ¬ LC [2a, = comm V]
[3] [CO Λ {RR Λ (¬ RR V (¬LC V ¬ CO))}] => ¬ LC [2b, = rassoc Λ]
[4][CO Λ {(RR Λ ¬ RR) V (RR Λ (¬ LC V ¬ CO))}] => ¬ LC [3, = dist ΛV]
[4a][CO Λ {(RR Λ ¬ RR) V (RR Λ ¬ LC) V (RR Λ ¬ CO)}] => ¬ LC [3, = dist ΛV]
[5] [CO Λ {false V (RR Λ ¬ LC) V (RR Λ ¬ CO)}] => ¬ LC [4a, =contr]
[6] [CO Λ {(false V (RR Λ ¬ LC)) V (RR Λ ¬ CO)}] => ¬ LC [5, =lassocV]
[6a] [CO Λ {((false V RR) Λ (false V¬ LC)) V (RR Λ ¬ CO)}] => ¬ LC [6, =distVΛ]
[6b] [CO Λ {((RR V false) Λ (¬ LC V false)) V (RR Λ ¬ CO)}] => ¬ LC [6a, =commV] *yes, I did two at once – but they’re the same
[6c] [CO Λ {(RR Λ ¬ LC) V (RR Λ ¬ CO)}] => ¬ LC [6b, =or3]
*yes, I did two at once – but they’re the same
[7] [CO Λ (RR Λ (¬ LC V ¬ CO)] => ¬ LC [6c, =dist ΛV]
[8] [CO Λ ((¬ CO V ¬ LC) Λ RR)] => ¬ LC [7, =comm Λ, =comm V]
[9] [CO Λ (¬ CO V ¬ LC) Λ RR] => ¬ LC [8, =rassoc Λ]
[10] [((CO Λ ¬ CO) V (CO Λ ¬ LC)) Λ RR] => ¬ LC [9, =lassoc Λ, =distr ΛV]
[11] [(false V (CO Λ ¬ LC)) Λ RR] => ¬ LC [10, =contr]
[12] [((false V CO) Λ (false V ¬ LC)) Λ RR] => ¬ LC [11, = distr VΛ]
[13] [((CO V false) Λ (¬ LC V false)) Λ RR] => ¬ LC [12, = comm V]
[14] [CO Λ ¬ LC Λ RR] => ¬ LC [13, = or3]
[15] ¬ [CO Λ ¬ LC Λ RR] V ¬ LC [14, = impl]
[16] ¬ [CO Λ (¬ LC Λ RR)] V ¬ LC [15, = rassoc Λ]
[17] {¬ CO V ¬ (¬ LC Λ RR)} V ¬ LC [16, = DeM Λ]
[18] {¬ CO V ¬ ¬ LC V ¬RR} V ¬ LC [17, = DeM Λ]
[19] ¬ CO V LC V ¬RR V ¬ LC [18, = neg, =lassoc]
[20] ¬ CO V LC V ¬ LC V ¬RR [19, = commV, =rassoc]
[21] ¬ CO V ¬RR V true [20, = commV, =rassoc, =exmid]
[22] ¬ CO V true [21, =rassoc, =or2]
[23] true [22, =or2]
NOTE: The book chose to deal with the left side of the problem (in []s and before the second implication. They then added in the second implication. So the book’s [4] is the left side of my [14]:
[4] ChannelOpen Λ ReceiverReady Λ ¬ LineClosed [3, = or3]
Here is where they put back the second implication:
To demonstrate the tautology it is thus necessary to show that
ChannelOpen Λ ReceiverReady Λ ¬ LineClosed => ¬ LineClosed
[pr] ChannelOpen Λ ReceiverReady Λ ¬ LineClosed => ¬ LineClosed
[1] ¬ (ChannelOpen Λ ReceiverReady) V LineClosed V ¬ LineClosed [pr, = impl, = DeM Λ ]
[2] ¬ (ChannelOpen Λ ReceiverReady) V true [1, = exmid]
[3] true [2, = or2]
Example 6
A system specification contains the sentences:
1. If the operator types the ALARM command, then the subsidiary alarm will be activated and an alarm message will be written to the log file.
2. Whenever the subsidiary alarm is activated, the main valve is closed and shut-down is started.
3. If the main valve is closed then the reactor can be regarded as being in a non-operational state.
Express these sentences in propositional calculus. Also show that if alarm command is activated the reactor will be in a non-operational state.
Solution
The propositions are
S1: Alarm => subsid Λ AlarmMessage
S2: Subsid => ValveClosed Λ ShutDown
S3: ValveClosed => NonOp
We shall label the above propositions S1, S2, and S3 in order to demonstrate
Alarm |─ Nonop
This is shown as follows. First S1 and S2 are substituted in the predicate giving the first line of the proof.
[pr] alarm Λ (alarm=> subsid Λ AlarmMessage) Λ (subsid => ValveClosed Λ ShutDown) Λ S3 => NonOp
[1] (alarm Λ subsid Λ AlarmMessage) Λ (subsid => ValveClosed Λ ShutDown) Λ S3 => NonOp [pr, = imp, = dist Λ V, = contr, = or3]
[1] (alarm Λ subsid Λ AlarmMessage) Λ (subsid => ValveClosed Λ ShutDown) Λ S3 => NonOp [pr, = imp, = dist Λ V, = contr, = or3]
[2] alarm Λ subsid Λ AlarmMessage Λ ValveClosed Λ ShutDown Λ S3 => NonOp [1, = imp, = contr, = and3, = or3]
[3] alarm Λ subsid Λ AlarmMessage Λ ValveClosed Λ ShutDown Λ (ValveClosed => NonOp) => NonOp [Substitution]
[4] alarm Λ subsid Λ AlarmMessage Λ ShutDown Λ ValveClosed Λ NonOp => NonOp [3, = impl, = dist Λ V, = contr, = or3]
[5] ¬ (alarm Λ subsid Λ AlarmMessage Λ ShutDown Λ ValveClosed Λ NonOp) V NonOp [4, = impl]
[6] ¬ (alarm Λ subsid Λ AlarmMessage Λ ShutDown Λ ValveClosed) V ¬ NonOp V NonOp [5, = DeM Λ]
[7] ¬ (alarm Λ subsid Λ AlarmMessage Λ ShutDown Λ ValveClosed) V true [6, = exmid]
[8] true [7, =or2]
RULES_OF_INFERENCE.pdf
RULES OF INFERENCE
p1 p1∨ = or1 true p1∨ = or2 false p1∨ =or3 p1 true p1
p2)p1( p1 ∧∨ = or4 p1 or5 p1 p2 p1∨
p1p1∧ =and1 truep1∧ =and2 falsep1∧ =and3
p1 p1 false
p2)p1( p1 ∨∧ =and4 p2,p1 =and5 p1 p2p1∧
p2p1∧ =comm ∧ p2p1∨ =comm ∨ p2p1⇔ =comm ⇔ p1p2∧ p1p2∨ p1p2 ⇔
p3p2 p1 ∧∧ =rassoc ∧ p3p2 p1 ∧∧ =lassoc ∧ p3)p2( p1 ∧∧ p3p2) (p1 ∧∧
p3p2 p1 ∨∨ =rassoc ∨ p3p2 p1 ∨∨ =lassoc∨ p3)p2( p1 ∨∨ p3p2)(p1 ∨∨
p3)p2( p1 ∧∨ =dist ∧∨ p3)p2( p1 ∨∧ =dist ∨∧ p3)(p1p2)(p1 ∨∧∨ p3)(p1p2)(p1 ∧∨∧
p2)p1( ∨¬ =DeM ∨ p2)p1( ∧¬ =DeM ∧ p2p1 ¬∧¬ p2p1 ¬∨¬
p1¬¬ =neg p1p1 ¬∨ =exmid p1p1 ¬∧ =contr
p1 true false
p2p1⇒ =impl p2p1p1, ⇒ implies p2p2,p1 ¬⇒ impliesnot p2p1∨¬ p2 p1¬
p2p1 ⇔ =equal
p1)(p2p2)(p1 ⇒∧⇒
∨p1 e p2 =exor p2p1p2p1 ∧¬∨¬∧
p2p2,p1 ¬⇔ equiv
p1¬
Exercise 3.5 1-3 answer.docx
Exercise 3.5
i.
|
PR |
open, open v steady |- open |
Reference |
Rule |
|
1 |
open ^ (open v steady) |- open |
PR |
=and5 |
|
2 |
open ^ (open v steady) => open |
1 |
proposition |
|
3 |
open => open |
2 |
=and4 |
|
4 |
¬open V open |
3 |
=impl |
|
5 |
TRUE |
4 |
=exmid |
|
6 |
|
5 |
|
|
7 |
|
6 |
|
|
8 |
|
7 |
|
ii.
|
PR |
test, functioning |- test ^ functioning |
Reference |
Rule |
|
1 |
test ^ functioning => test ^ functioning |
PR |
=and5 |
|
2 |
¬(test ^ functioning) v (test ^ functioning) |
1 |
=impl |
|
3 |
TURE |
2 |
=exmid |
|
4 |
|
3 |
|
|
5 |
|
4 |
|
|
6 |
|
5 |
|
|
7 |
|
6 |
|
|
8 |
|
7 |
|
iii.
|
PR |
receiving, receiving => open, open |- receiving v closed => open (R = receiving, O = open, C = closed) |
Reference |
Rule |
|
1 |
R ^ (R=>O) ^ O => (R v C => O) |
PR |
=and5, =impl |
|
2 |
R ^ (¬R v O) ^ O => (¬(R v C) v O) |
1 |
=impl |
|
3 |
R ^ O => (¬(R v C) v O) |
2 |
=and4 |
|
4 |
¬(R ^ O) v ¬(R v C) v O |
3 |
=impl |
|
5 |
¬R v ¬O v ¬(R v C) v O |
4 |
=DeM^ |
|
6 |
¬R v ¬(R v C) v TRUE |
5 |
=exmid |
|
7 |
TRUE |
6 |
=or2 |
|
8 |
|
7 |
|
Table of Contents.html
| Frml Meth. Software E XLS Group CA Spring Semester 2018 CO - Week 6
2. note_for_indirect_proofV2.doc |
