Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
sav08:tools_demo [2008/02/21 22:53] piskac |
sav08:tools_demo [2008/02/22 10:44] piskac |
||
---|---|---|---|
Line 58: | Line 58: | ||
| | ||
end_of_list. | end_of_list. | ||
- | + | | |
- | + | end_problem. | |
- | end_problem. | + | |
===== formDecider - part of Jahob ===== | ===== formDecider - part of Jahob ===== | ||
Line 88: | Line 87: | ||
The last argument denote the theorem prover invoked. It can also be: | The last argument denote the theorem prover invoked. It can also be: | ||
- | formDecider.opt killer.form -usedp e [[http://www.eprover.org/|E theorem prover]] | + | formDecider.opt killer.form -usedp e |
formDecider.opt killer.form -usedp vampire | formDecider.opt killer.form -usedp vampire | ||
formDecider.opt killer.form -usedp cvcl | formDecider.opt killer.form -usedp cvcl | ||
Line 94: | Line 93: | ||
+ | The theorem provers that formDecider invokes are: | ||
+ | * e = [[http://www.eprover.org/|E theorem prover]] | ||
+ | * vampire = [[http://en.wikipedia.org/wiki/Vampire_theorem_prover|Vampire theorem prover]] | ||
+ | * cvcl = [[http://www.cs.nyu.edu/acsys/cvc3/|CVC3 theorem prover]] | ||
+ | * z3 = [[http://research.microsoft.com/projects/z3/|Z3 theorem prover]] |