IntroductionFirst Things First

We’ll return to the Philosophical Railway later. For now, let’s begin at the beginning by taking a look at the solver on the right side of the page.

You see a form with three boxes in which you may type text, plus a few buttons and such that you do not touch yet.

I said don’t touch yet!

Never mind what “Sorts”, “Vocabulary” and “Constraints” are for now. We’ll begin by posing the solver a really dumb problem, just to illustrate how things go. Let’s get it to solve the exciting equation:

I guess you can work out the answer without using your fingers – they told you that high school algebra would come in useful for something! The point, however, is not that you can do it but that you can get the computer to do it.

Nothing simpler! In the “Constraints” box, type:

2 + x = 4.

Don’t forget the period after the “4”, as it tells the solver this is the end of the equation. We can check that the syntax is OK (at least that it gets past the parser) by hitting the “Check syntax” button. It may warn us that we are using the expression “x” as the name of an unknown number without declaring it as such, but that’s OK in this case, as we intend it to be just that. Now if we hit the “Solve” button (bottom right on the form) we should get the answer in the box marked “Solver output” below the buttons:

Model 1: x = 2.

The solution (2, of course) tells us what value we have to substitute for “x” to get whatever is in the “Constraints” box to come out true. That’s what it means by a “model” of the constraints.