ButtonsNuts And Bolts

At the bottom of the solver input form, along with the CHECK and SOLVE buttons, are several others :

• Load solution
• Save solution
• Submit to class
• Settings
• Diagnose
  The last two of these are the subjects of their own pages of this guide. This page outlines the use of the others along with the options at the top of the page:
• Learn
• Puzzles
• Solver
• Feedback
• My account

Solve
The SOLVE button causes the contents of the three boxes on the form to be passed to a finite-domain constraint solver which parses the text, compiles it into constraints and searches for solutions. The output is written in plain text and appears below the boxes. If the solver times out or otherwise terminates without finding solutions, it prints a brief message to that effect instead.

Check syntax
The CHECK button acts exactly like SOLVE, except that the reasoning software is instructed to stop after parsing and type-checking the input. The output is either a statement that the syntax is OK or else an error message of some kind. The fact that the text gets past the parser does not, of course, mean that it is correct, but only that it makes some sort of sense.

Save solution
The SAVE button causes your problem encoding to be stored so that you can go back to it later. It does not matter if you then logout and login again: the saved work will still be available. You are prompted to give the saved work a name, for easy recall. If you are working on a complicated problem or it is taking a long time, you may find it a good idea to save from time to time in order to create checkpoints to which you can revert if things seem to be going wrong later.

Load solution
LOAD is simply the opposite of SAVE. It reads the named problem encoding back into the three boxes, over-writing whatever happens to be there.

Submit to class
SUBMIT sends your work to the class administrator. This may be done in order to get feedback on it, or for purposes of course assessment, for instance. In order for submission to be possible, the class manager must have set up a submission group (an assignment, for example) and given it a name. If there is a submission group available, it will appear in the drop-down list : just select it and submit. If you submit work more than once to the same submission group, the latest version over-rides any earlier ones.

Learn
The LEARN option takes you to this guide from any page. For a more detailed account of first order logic, see The Logic Notes.

Puzzles
The PUZZLES option links to the index of the pre-defined puzzles. These are grouped by level, roughly corresponding to degree of difficulty:

1. Beginner : simple sentence structures, no complicated sorts or function symbols; can be encoded in a few short lines.
2. Intermediate : mostly puzzles of the sort found in logic magazines; typically do not involve existential quantifiers or partial functions; heavy use of bijective functions.
3. Advanced : not much harder than the intermediate puzzles, but requiring more features of first order logic, including nested quantifiers and partial functions.
4. Expert : distinctly harder; several requiring problems about state transition systems to be encoded, for instance to produce plans for reaching a goal.
5. Logician : similar to the puzzles in the expert list, but moving more towards applications of logic to matters outside itself and to less artificial problems.
6. Insane : these problems may be impossible, as in their natural formulations they are not expressible in first order logic! It is interesting to see how close you can get to solving them, however.

Solver
The SOLVER button allows you to access the three boxes for typing in problems, without going through any particular puzzle.

Feedback
The FEEDBACK button leads to forms for reporting bugs or for commenting on any aspect of the site. These are fairly self-explanatory.

My account
Use this button at the top right of your browser window to check or edit your user details, join classes or logout.