I wrote it when I was taking the class even though it took much more time than actually doing the two or three problems (I was only taking the second half of the course, in which the sort of problems for which it can provide results have less prominence) for which it works took. I make it public now because I just remembered it? The textbook poses certain problems in terms of either finding a model for a bunch of statements or providing a counterexample to a claim, where the world in which one does this is of blocks of various sizes, shapes and positions; predicates are, eg, "is small" or "is to the right of" or "is the same shape as". Here's the script; a sample input module has a little explanation. If 15-32.py is in one's import path, then one can do this:
$ python /path/to/board.py 15-32
a: Cube(2,1,small)
b: Tetrahedron(0,1,small)
c: Cube(2,1,small)
$
The output being, of course, the names and natures of the blocks constituting a solution (in this case a counterexample to a claim about a relation's transitivity, with one object having two names). Since for any problem it's the case that either a model can be constructed to do the right thing (whatever that might be) or a proof can be constructed showing that the right thing can't be done, if one attempts to find a solution with this script and none is generated (assuming it's got no bugs, that is), that constitutes, at least pragmatically, a proof that none can be generated. Unfortunately, the program used to grade these things is an intuitionist and demands a postive proof.
Recent Comments