22c:245 - Advanced Artificial Intelligence

Spring 2004

Final Projects

For the final project you have the choice of doing an implementation project or an experimental one. All projects are team projects.

Teams

Although you will work on a project in a team, the grade for the project will be given on an individual basis. All students will be asked to submit evaluations (on a form provided by the instructor) of how well they and their teammates are performing as team members. Each evaluation is confidential and will not be shown to other team member. The evaluations will be incorporated into the calculation of the project grade.

Part of the educational objective of these projects is to work in a team of people with diverse backgrounds, skills, and personalities. As a consequence, the teams are assembled by the instructor.

The teams for this semester are the following:

  1. Barbara, Colin
  2. Gaurav, Meredith
  3. Guarionex, John
  4. Justin, Menny
  5. Mike, Wenwu

Implementation Projects

The implementation projects consist in modifying a prototype prover, written in Ocaml, for the Model Evolution calculus. Please see the instructors for more details on project requirements.

Experimental projects

The experimental projects consist in experimenting with one of the theorem provers listed below and then report results in a in a brief presentation and in a final report. For this project, you will need to:
  1. Download the prover from the web and install it on a lab machine (or your own).
  2. Study the prover's documentation; manuals, tutorials, and/or one or two related papers provided on the prover's web site.
  3. Choose some input problems from a problem library provided by the instructor, run the prover on them and collect various statistics, including at the very least, run time. Other statistics (such as number of expanded nodes/resolutions/subsumptions etc.) are prover dependent and may be generated by setting appropriate flags in the prover.
  4. Prepare a 15-20 minute presentation that briefly describes:
    1. The prover itself (based on the documentation you read).
    2. The experiments your carried out with the prover (listing the problems you tried and a number of statistics on them).
    3. Everything else you learned or found relevant.

The problem library will be available on the lab linux machines in the directory /group/class/c245/benchmarks/.

Presentation Date and Times

All presentations are scheduled for Wednesday, May 12.

Time Team System Project Type
12:00-12:25pm 3 Darwin Impl.
12:25-12:50pm 1 DCTP Exp.
12:50-01:15pm 4 SPASS Exp.
01:15-01:40pm 2 Darwin Impl.
01:40-02:05pm 5 E Exp.

Contact the instructor as soon as possible to schedule your presentation in one of these time slots.

Suggested theorem provers

Descriptions of these systems, information on how to get them, and a set of benchmarks can be found on the web site of the CADE-19 ATP System Competition.

Last Updated: April 19, 2004