Differences
This shows you the differences between two versions of the page.
Next revision Both sides next revision | |||
sav08:exercise_06 [2008/03/20 19:12] vkuncak created |
sav08:exercise_06 [2008/03/20 19:18] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Exercise 06 - DRAFT ====== | ====== Exercise 06 - DRAFT ====== | ||
- | Build a resolution-based theorem prover that will win the [[http://www.cs.miami.edu/~tptp/CASC/|CASC competition]] of resolution-based theorem provers. | + | Build a theorem prover that will win the [[http://www.cs.miami.edu/~tptp/CASC/|CASC competition]] of resolution-based theorem provers. |
+ | |||
+ | You may wish to consult the following: | ||
+ | * [[http://portal.acm.org/citation.cfm?id=606318.606321|The design and implementation of VAMPIRE]] | ||
+ | * [[http://spass.mpi-sb.mpg.de/|SPASS]] | ||
+ | * [[http://citeseer.ist.psu.edu/560030.html|E: A Braniac Theorem Prover]] | ||