Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:tools_demo [2008/02/21 23:00] 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 97: | Line 96: | ||
* e = [[http://www.eprover.org/|E theorem prover]] | * e = [[http://www.eprover.org/|E theorem prover]] | ||
* vampire = [[http://en.wikipedia.org/wiki/Vampire_theorem_prover|Vampire theorem prover]] | * vampire = [[http://en.wikipedia.org/wiki/Vampire_theorem_prover|Vampire theorem prover]] | ||
- | * cvcl = | + | * cvcl = [[http://www.cs.nyu.edu/acsys/cvc3/|CVC3 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. |