Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:tools_demo [2008/02/21 22:49] piskac |
sav08:tools_demo [2008/02/21 23:00] piskac |
||
|---|---|---|---|
| Line 81: | Line 81: | ||
| (killed :: obj => obj => bool) a a | (killed :: obj => obj => bool) a a | ||
| + | |||
| + | formDecider is invoked using the following command: | ||
| + | |||
| + | jahob/bin/formDecider.opt killer.form -usedp spass | ||
| + | |||
| + | The last argument denote the theorem prover invoked. It can also be: | ||
| + | |||
| + | formDecider.opt killer.form -usedp e | ||
| + | formDecider.opt killer.form -usedp vampire | ||
| + | formDecider.opt killer.form -usedp cvcl | ||
| + | formDecider.opt killer.form -usedp z3 | ||
| + | |||
| + | |||
| + | 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 = | ||