LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:tools_demo [2008/02/21 23:06]
piskac
sav08:tools_demo [2010/02/26 20:20]
hossein
Line 58: Line 58:
   ​   ​
   end_of_list.   end_of_list.
- +  ​ 
- +  end_problem.
-end_problem.+
  
 ===== formDecider - part of Jahob ===== ===== formDecider - part of Jahob =====
Line 99: 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.