A rule is a series of structures in which the truth of the first structure follows from the ability to prove the remaining structures. For example, in Logikus the following rule defines "high" cities:
highCity(Name, Alt) :- city(Name, Alt), >(Alt, 5000);
This rule states that highCity(Name, Alt) is true for any known city whose altitude is greater than 5,000. A rule's first structure is its head; its other structure is its tail. Between its head and its tail a rule has the "if" (" :- " ) symbol. The head is true if the tail is provable.
An axiom is a model of truth, and in Logikus an axiom is either a fact or a rule. A Logikus program is a collection of axioms, and this means that a program is an extended model of some truth in some context. For example, a collection of facts about city altitudes combined in a program with the highCity rule lets you query the program to ask which cities are high. Figure 13.2 shows such a program using data from the CD file city.txt .
Figure 13.2. A rule in action. The highCity rule lets a query find which cities in a collection are, in fact, high.
In Figure 13.2, the query succeeds because it is able to unify with the head of a rule whose tail can, in turn , prove itself. In the figure, the user has pressed the Rest button, asking for all the proofs. The behavior of the query and the rule depends primarily on the mechanics of proofs.