• English only

Differences

This shows you the differences between two versions of the page.

sav08:tools_demo [2008/02/22 10:44]
piskac
sav08:tools_demo [2010/02/26 20:20] (current)
hossein
Line 98: Line 98:
* cvcl = [[http://​www.cs.nyu.edu/​acsys/​cvc3/​|CVC3 theorem prover]]   * cvcl = [[http://​www.cs.nyu.edu/​acsys/​cvc3/​|CVC3 theorem prover]]
* z3 = [[http://​research.microsoft.com/​projects/​z3/​|Z3 theorem prover]]   * z3 = [[http://​research.microsoft.com/​projects/​z3/​|Z3 theorem prover]]
+
+===== Isabelle/​HOL =====
+
+  * Install the [[http://​isabelle.in.tum.de/​|Isabelle/​HOL]] theorem prover and test it on "​Dreadbury Mansion Mystery"​ example:
+
+
+  theory aunt
+  imports Main
+  begin
+  theorem agatha:
+  assumes a1 : "​EX ​ x.(lives(x) & killed(x, a))"
+  and     a2 : "​lives(a) & lives(b) & lives(c) & (ALL x. (lives(x) --> (x=a | x=b | x=c)))"​
+  and     a3 : "ALL x. ALL y. (killed(x,​y) --> (hates(x,y) & ~richer(x,​y)))"​
+  and     a4 : "ALL x. (hates(a,x) --> ~hates(c,​x))"​
+  and     a5 : "ALL x. (hates(a,x) = (x ~= b))"
+  and     a6 : "ALL x. ((~richer(x,​a)) = hates(b,​x))"​
+  and     a7 : "ALL x. (hates(a,x) --> hates(b,​x))"​
+  and     a8 : "~(EX x. ALL y. hates(x,​y))"​
+  and     a9 : "a ~= b"
+  shows   "​killed(a,​a)"​
+  using a1 a2 a3 a4 a5 a6 a7 a8 a9 sledgehammer e
+  end
+
+
+In the specification we invoke [[http://​www4.informatik.tu-muenchen.de/​~schulz/​WORK/​eprover.html|E]] for proving the formulas.