More About ClausesReally Advanced Topics

The syntax of atoms is the same for the purpose of clauses as it is for first order formulae, but the solver does not always treat them in the same way. Consider the example given to the right of this page. If you click the “Solve” button, you will see the obvious solution:

 Model 1

 person | 0     1
 –––––––+––––––––––––
    man | TRUE  FALSE  

 person | 0      1
 –––––––+––––––––––––
  woman | FALSE  TRUE

 Tom = 0 

 Mary = 1 
 

and a second model in which the roles of 0 and 1 are reversed. However, if you change the settings by turning on clause form, you get:

  No solution found.

What is going on?

The answer is that in full first order notation the expressions “Tom” and “Mary” are parsed as names, but in clause form they are parsed as variables, like the x in the first constraint. Since they are not explicitly bound by quantifiers, they are called free variables. The reading of a clause containing free variables is the same as if they were bound by universal quantifiers standing outside the whole clause. Hence the clauses

man(Tom).
woman(Mary).

are read as if they were

ALL Tom man(Tom).
ALL Mary woman(Mary).

That is, they assert that everyone is a man and everyone is a woman, contradicting the first clause which says that nobody is both—hence the lack of solutions.

In order to cause “Tom” and “Mary” to be read as names, we must explicitly declare them as such. That is, in the Vocabulary box, we must write

name Tom: person {}
name Mary: person {}

The reason for reading undeclared identifiers as free variables rather than names is to enable the notation to get by without explicit universal quantifiers: since every variable is universally bound, there is no need for them.

Existential quantifiers are another matter. Where a clause asserts existence, we declare a “nonce” name, annotate it as “hidden” and then use it to refer to an arbitrary one of the things asserted to exist. The effect is the same as if we used an existential quantifier.

If the existential quantifier is inside the scope of a universal one, we must introduce not an arbitrary name but an arbitrary function symbol with an argument place, because it may need to pick out different things for different values of the universal variable. Such a function is called a Skolem function and the process of removing existential quantifiers in this way is known as skolemisation. See the next page for a fuller description and some examples.