| << Prev | - Up - | Next >> |
Problems with free variables in input formulae.
We run into similar trouble if we feed our model checker formulae with free variables (i.e. ones that are not bound by a quantifier). For example evaluate(therapist(x),1). Our model checker answers no, although formally, truth in a model is only defined for sentences, i.e. formulae with no free variables. There are ways of extending this definition to formulae with free variables (see Exercise 2.10). But since we have not chosen any of these extensions, we needn't implement them. We will simply refuse non-sentences, just as we will refuse non-well-formed formulae.
| << Prev | - Up - | Next >> |