Clause FormReally Advanced Topics
NOTE: If there is no “clause form” button in the settings, this option has been disabled. In that case, ignore the guide pages about clauses, as they do not apply.
Most of the puzzles on this site are written on the assumption that you will express them in full first order logic, using the standard connectives and quantifiers to be found in any logic textbook. Behind the scenes, however, your first order formulae are transformed into a simpler fragment of the language in which there are no quantifiers and in which connectives occur only in a tightly controlled way. This is clause form, which is a bit cumbersome for human beings to read and write (though you can become fluent in it) but is standard in automated reasoning because of its simplicity.
The clause form setting, which can be selected via the Settings button, makes the solver accept a clausal language in which the connectives and quantifiers still exist but can always be defined away if we wish. It is worth learning this version of first order logic, even if you rarely use it in practice, as it may help you to understand how the solver sees your formulae—and also to read what it reports if you ask it to print the job.
A clause is a statement of the form
A 1 , … , A k -> C 1 ; … ; C m .
where A 1, …, A k is a list of (zero or more) atoms separated by commas (,) and C 1 ; …; C m is a list of (one or more) atoms separated by semicolons (;). The arrow is written as a hyphen followed by “greater than”. The atoms in A are called the antecedents and those in C are called the consequents of the clause. Sometimes the consequents are called the head and the antecedents the body of the clause. The intended reading is that if all of the antecedents are true, then so is at least one of the consequents. The clause must end with a period (.). There must be at least one consequent (and may be more) but the list of antecedents may be empty, in which case we may optionally omit the arrow.
So what is an “atom”? It is any formula of the form:
B(t 1 , …, t n )
where B is an n-adic relation (i.e. predicate) symbol and where each t i is a term of the appropriate sort to go in the i-th argument place of B. Often B is one of the built-in relation symbols such as “=”, or a built-in connective like “NOT” or “AND”, but it does not have to be. The special case where n = 0 (meaning B is just a proposition, with no argument places) is allowed.
Now, a “term” is either a variable, a canonical name (from the “enum” list of a sort) or an expression of the form
f(t 1 , …, t n )
where f is an n-adic function symbol and t 1 , …, t n are terms of the appropriate sorts. Again the case n = 0 (where f is just a name and there are no arguments) is allowed. Note that binary function symbols, like binary relation symbols, may be written in infix position (like the “+” in “a + b”) rather than prefix. This is simply to help readability. Atoms are exactly the same whether we are writing in clause form or in the usual first order notation.
Here are a few examples to show different clause structures:
| Tom loves Mary. | Clause with no antecedents and one consequent |
| Tom loves Mary ; Tom loves Jane. | Two consequents: Tom loves either Mary or Jane |
| Tom loves Mary -> happy(Mary). | One antecedent, one consequent: if Tom loves Mary, she is happy |
| T loves M , M loves T -> happy(T) ; happy(M). | Two antecedents and two consequents: if Tom and Mary love each other, at least one of them is happy |
You will see that the comma, the semicolon and the arrow have the same semantics as AND, OR and IMP respectively, and indeed in a sense they are those connectives, but in clauses they are not allowed to occur nested one inside the other except as shown, so they can also be viewed just as separators between the atoms.