<< Prev | - Up - | Next >> |

Description of important helper predicates often used in the course.

The predicate `compose/3`

(de-)composes complex terms out of (into) the functor and a list of its arguments. Possible usage:

| |

| |

`newvar(-NewVar)`

This predicate returns in its argument a new variable according to our convention: `v1,v2,...,vn`

.

Each call of `resetVars/0`

sets the variable counter back to 0.

`printRepresentations(+Terms)`

Prints all complex terms from its input *list* in a human readable fashion. Each term is put in a new (numbered) line. Second, the Prolog variables are displayed as capital letters (or the like, this is done by the Prolog built-in predicate `numbervars/3`

).

Note that the variables are replaced for each term (from `Terms`

) beginning from scratch. So, variable coindexing between terms (from line to line) is not possible (see the example below). Coindexing within one term is handled, of course.

`printRepresentations([p(MyVar1),q(MyVar2),r(MyVar1,MyVar2),r(MyVar1,MyVar1),z(_,_)]).`

`readLine(-AtomList)`

The auxiliary predicate `readLine/1`

prompts the user to type in a sentence and returns our well-known list representation of the sentence. If the user types in ``John walks'', `readLine/1`

instantiates its argument with [john,walks].

`substitute(+Term,+Var,+InFormula,?OutFormula)`

This predicate implements a version of the Sterling and Shapiro `substitute/4`

predicate. It takes a term, a variable, and a formula as its first three arguments, and returns in its fourth argument the result of substituting the term for each free occurrence of the variable in the formula. Because this is an important predicate (we shall use it again when we implement a first-order theorem prover), we recommend that you look at its definition.

`substitute(woman,P,lambda(Q, exists(X,P@X& Q@X)),Result), printRepresentations([Result]). `

`vars2Atoms(-Term)`

The predicate `vars2atoms/1`

extracts all free (Prolog-) variables from the input term with the help of the Prlog in-built predicate `free_variables/2`

. These variables then are instantiated with fresh and distinct variables using `newvar/1`

(see Section ``newvar/1'').

`vars2atoms(lambda(A, A@tweety)@lambda(B, smoke(B))),write(lambda(A, A@tweety)@lambda(B, smoke(B)))`

Calling `resetVars`

(see Section ``newvar/1'') resets the variable counter.

<< Prev | - Up - | Next >> |

Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos

Version 1.2.5 (20030212)