30 lines
934 B
Plaintext
30 lines
934 B
Plaintext
theory Enigme
|
|
|
|
predicate a
|
|
predicate b
|
|
predicate c
|
|
|
|
predicate da = b /\ (not c)
|
|
predicate db = a -> c
|
|
predicate dc = (not c) /\ ( a \/ b )
|
|
|
|
goal Q1: not (da /\ db /\ dc)
|
|
(* on demande ensuite un contre exemple *)
|
|
|
|
goal Q2c: da /\ db -> dc (* vrai *)
|
|
goal Q2b: dc /\ da -> db (* faux *)
|
|
goal Q2a: db /\ dc -> da (* vrai *)
|
|
|
|
goal Q3a: (not a) /\ (not b) /\ (not c) -> da (* faux, a ment *)
|
|
goal Q3b: (not a) /\ (not b) /\ (not c) -> db (* b dit la vérité *)
|
|
goal Q3c: (not a) /\ (not b) /\ (not c) -> dc (* faux, c ment *)
|
|
|
|
goal Q4a: da /\ db /\ dc -> a (* faux, a innocent *)
|
|
goal Q4b: da /\ db /\ dc -> b (* b coupable *)
|
|
goal Q4c: da /\ db /\ dc -> c (* faux, c innocent *)
|
|
|
|
goal Q5: not ( (a -> (not da)) /\ (b -> (not db)) /\ (c -> (not dc)) )
|
|
(* on demande ensuite un contre exemple *)
|
|
|
|
end
|