Commit 952cc543 authored by MARCHE Claude's avatar MARCHE Claude

new example: scottish club

parent b402afbd
*~
*.bak
*.o
*.svn
.*.swp
......@@ -45,13 +46,14 @@ why.conf
/bin/why3-cpulimit
/bin/whyconfig.byte
/bin/whyconfig.opt
/bin/whydb.byte
/bin/whydb.opt
/bin/whybench.byte
/bin/whybench.opt
/bin/whytptp.byte
/bin/whytptp.opt
# /doc/
/doc/version.tex
/doc/ocamldoc.sty
/doc/*whizzy*
/doc/manual.wdvi
/doc/manual.raux
......@@ -63,6 +65,7 @@ why.conf
/doc/manual.ind
/doc/manual.ilg
/doc/manual.idx
/doc/manual.rel
/doc/*.haux
/doc/*.pdf
/doc/manual.html
......@@ -160,4 +163,8 @@ why.conf
/src/util/rc.ml
# /tests/
/tests/*.db
/tests/test-claude/
# /examples/
/examples/programs/my_cosine/*.gappa
/examples/scottish-private-club/
\ No newline at end of file
(*
The classical example of the Scottish private club puzzle
The club follows six rules:
- every non-scottish members wear red socks
- every member wears a kilt or doesn't wear socks
- the married members don't go out on sunday
- a member goes out on sunday if and only if he is scottish
- every member who wears a kilt is scottish and married
- every scottish member wears a kilt
Problem: prove that there is nobody in this club !
*)
theory ScottishClubProblem "the Scottish private club puzzle"
type member
logic is_scottish member
logic wears_red_socks member
logic wears_kilt member
logic is_married member
logic goes_out_on_sunday member
axiom R1: forall m:member. not (is_scottish m) -> wears_red_socks m
axiom R2: forall m:member. wears_kilt m or not (wears_red_socks m)
axiom R3: forall m:member. is_married m -> not (goes_out_on_sunday m)
axiom R4: forall m:member. goes_out_on_sunday m <-> is_scottish m
axiom R5: forall m:member. wears_kilt m -> is_scottish m and is_married m
axiom R6: forall m:member. is_scottish m -> wears_kilt m
goal ThereIsNobodyInTheClub: false
end
theory TestProp
logic a
logic b
goal Test1: a and b -> a
end
theory TestInt
use import int.Int
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment