5.2.5 Formulas are trees!

Formulas can be written as trees.

Tree Notation

We've just said that we're going to develop a formalism that allows us to describe trees. But why trees? Shouldn't we talk about formulas? The answer is that formulas are trees - if you look at them the right way. Representing formulas as trees is simple. You know that every formula of first order logic has a main connective. For instance, a conjunction has the main connective and the subformulas and . So if we know how to represent the two subformulas as trees, we can represent the whole formula as a tree whose root node is labeled with the symbol and the two trees for and as children. This works similarly with the other connectives. The leaves of the tree are predicate symbols, constants, and variables.

New Representation of Atomic Formulae!

Finally, on the level of atomic formulas, we shall from now on write application of predicates to arguments with the binary symbol . (We have already seen this: We indicate applications in -calculus the same way). Here's one of our standard example formulae in this notation (if you're interested in the motivation behind our decision to use this new notation, read the sidetrack at the end of this chapter):

Now have a look at the following tree representation of this formula:

Testtitel

?- Question!

In one respect, the tree above differs from the formula it represents. Do you see where?

Binding Edges

The answer to this question is that variables are represented differently in the tree representation. We could have used variable names as we always have. But we will see later that this would have lead us into problems when writing underspecified descriptions. That's why we explicitly link bound variables to their binders via binding edge s. These are depicted as purple arrows in the picture above. Since these binding edges tell us all there is to know about which variables are bound by which binders, we can do away with variable names altogether, and it is sufficient to label variable nodes with the symbol and quantifier nodes with the symbols and . We will see in the implementation section that this way of handling variable binding will even simplify our implementation.