Raft

In the summer of 2004 my friend Michael Beeson visited our department for a couple of weeks, and during this visit we discussed his plans to prove serious mathematical theorems using his Otter-lambda program.

Right after that discussion I wrote a small perl script intended to help with this work. As it deals with a whole set of Otter input files, I tried to find out what a group of otters is called (a flock? a swarm? a herd?) And so I learned that one talks about a raft of sea otters. (It's particularly nice that it's about sea otters, as Michael's home is near a beach where many of those sea otters live.) So I named my little script raft.

So here are

• the perl script called raft itself
• the example input file groups.raft

The way to install this is to download the raft script, make it executable, and put it in a place like /usr/local/bin where scripts will be found. (Edit the first line of the script if your perl is somewhere else & don't forget to do a rehash if that is necessary for your shell).

Then to use raft, create an input file yourfile.raft and invoke raft on it with:

raft yourfile.raft

A raft file is structured as a sequence of lemmas that look like:

LEMMA @lemmaname @lemmaclass
  statement
PROOF
otter input file template
QED

For every lemma raft will create three files, which are called lemmaname.in and lemmaname.out and lemmaname.log. The first is the Otter input file that is generated by raft. Although you can edit this file and call Otter on it yourself, that is not the way the system is meant to be used. Instead raft does this for you, putting the Otter output in the second file, and a one line description of how things went in the third. (Therefore, if you do cat *.log in a directory, you can easily see what is the status of all the files: which ones contain a successful proof, and which ones are not working yet.)

The raft script has functionality like "make": it will only rewrite an input file if anything in the raft source file has changed that affects the corresponding lemma, and it will only run Otter for the scripts in which anything has changed. For this reason, if you run raft twice on the same raft input file, the second time it will just print the contents of the ".log" files (with an added "(cached)" behind it, to show that it is doing this.) So for any input file it will invoke Otter just once.

You should work exclusively on the raft input file (which contains everything that is important anyway), and continuously "check" this file by invoking raft on it.

To try the system out, try running it on the groups.raft example file and see what happens. For a description of some of the features of raft, study the comments in that file. And in case you have remarks or a feature wish or anything, feel free to send me an e-mail about this little thing.

*

Ah yes. You cannot give statements to raft that are already in clausified form. This is because raft needs to put the statements in the Otter files both themselves (when using them to prove later lemmas) as well as their negated form (when proving them themselves). If the statement had been clausified, it would have trouble doing this. So to use raft, you should unlearn doing clausification yourself. It's a pity, as the skolem functions will get strange names.

An important consequence of this is that you need to fully quantify all free variables in each statement. They need to be closed formulas! For instance it is wrong to write:

x * (y * z) = (x * y) * z

As raft uses formula_list(...) instead of list(...), in that case the x and y and z would be taken to be constants instead of variables. (I didn't know this, but Bill McCune enlightened me.) So instead one has to write the formula in fully quantified form:

all x y z (x * (y * z) = (x * y) * z)

(last modification 2004-09-03)