Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:homework06a [2008/03/20 19:23] vkuncak |
sav08:homework06a [2008/04/01 10:31] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Homework 06 - DRAFT ====== | + | ====== Homework 06 - Handed out on April 1 ====== |
- | Build a theorem prover that will win the [[http://www.cs.miami.edu/~tptp/CASC/|CASC competition]] of resolution-based theorem provers. | + | Build a first-order theorem prover. Make sure your prover ranks above Vampire in the [[http://www.cs.miami.edu/~tptp/CASC/|CASC competition]] of resolution-based theorem provers. |
- | You may wish to consult the following: | + | The following references might be helpful: |
- | * [[http://portal.acm.org/citation.cfm?id=606318.606321|The design and implementation of VAMPIRE]] | + | * [[http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=8574|Handbook of Automated Reasoning]] (only the first 1900 pages) |
+ | * [[http://portal.acm.org/citation.cfm?id=606318.606321|The design and implementation of VAMPIRE]] (and [[http://www.voronkov.com/|Voronkov.com]]) | ||
* [[http://spass.mpi-sb.mpg.de/|SPASS]] | * [[http://spass.mpi-sb.mpg.de/|SPASS]] | ||
* [[http://citeseer.ist.psu.edu/560030.html|E: A Braniac Theorem Prover]] | * [[http://citeseer.ist.psu.edu/560030.html|E: A Braniac Theorem Prover]] | ||