Commit 703e0c3d authored by MARCHE Claude's avatar MARCHE Claude

propositional examples now work

parent f964bd96
......@@ -38,8 +38,10 @@
* INSTALL (done)
* LICENSE (done)
* OCAML-LICENSE (TODO: Andrei)
* TODO: licence pour les boomy icons
* option -version a tous les executables + affichage dans l'IDE (TODO)
* option -version a tous les executables (TODO)
** + affichage dans l'IDE (done)
* Builtin arrays in provers (TODO: Francois)
* make install (done)
* make export (TODO: JCF)
......
......@@ -3,8 +3,6 @@ prover = "alt-ergo"
prover = "cvc3"
timelimit = 5
[tools tptp]
prover = "spass"
[probs funny]
file = "talk290.mlw"
......
......@@ -22,25 +22,23 @@ Problem: prove that there is nobody in this club !
theory ScottishClubProblem "the Scottish private club puzzle"
type member
logic is_scottish
logic wears_red_socks
logic wears_kilt
logic is_married
logic goes_out_on_sunday
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: not is_scottish -> wears_red_socks
axiom R1: forall m:member. not (is_scottish m) -> wears_red_socks m
axiom R2: wears_kilt or not wears_red_socks
axiom R2: forall m:member. wears_kilt m or not (wears_red_socks m)
axiom R3: is_married -> not goes_out_on_sunday
axiom R3: forall m:member. is_married m -> not (goes_out_on_sunday m)
axiom R4: goes_out_on_sunday <-> is_scottish
axiom R4: forall m:member. goes_out_on_sunday m <-> is_scottish m
axiom R5: wears_kilt -> is_scottish and is_married
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
axiom R6: is_scottish -> wears_kilt
goal ThereIsNobodyInTheClub: false
......
theory TestProp
logic a int
logic b int
logic a
goal Test1: a 0 and b 1 -> a 0
logic b
goal Test1: a and b -> a
end
......
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