Predicates

The oRatio solver reasons in terms of first-order Horn clauses therefore each predicate is associated to a rule that must be complied with in order for the atom, unifying with the head of the rule, to be valid. Consequently, the language has been designed to define both predicates and rules together. Specifically, predicates (and rules) are defined through the following syntax:

predicate <id> (<type> <id>, <type> <id>, ...) {
  <rule body>
}

in which is represented the identifier of the predicate, a typed list of arguments, and the body of the rule. Suppose, for example, we are interested in representing the location of an agent, we might use the following rule:

predicate At (Location l) {
}

The arguments of the predicates are considered as existentially quantified variables within the body of the rule which might contain constraints on them and/or on other variables. Specifically, the body of the rule contains a list of statement which is executed for each atomic formula that does not unify. Suppose, for example, we want to express the fact that our agent cannot go on a location outside of the first quadrant of the Cartesian space, we might use the following rule:

predicate At(Location l) {
  l.x >= 0;
  l.y >= 0;
}

In some cases, it might be useful to see the body of a rule as the preconditions that must be respected in order for the atomic formula to be valid. The above example can be therefore rephrased as: in order for a robot for being at a given location, the location must be within the first quadrant of the Cartesian space.

Taking advantage of the similarity that a predicate (with its arguments) has a with complex type (with its members) the domain description language gives to the modeler the possibility to define inheritance among predicates, just as is the case of complex types. Just note that the body of the base rules will be executed before the body of the derived rule. The syntax for predicate inheritance is similar to the syntax used for type inheritance.

predicate LimitedAt() : At {
  l.x <= 10;
  l.y <= 10;
}

Predicates can be also defined within complex types. Each predicate defined within a class has an implicit parameter called tau, representing the τ variable of the corresponding atoms, of the same type within which the predicate has been defined. As an example, the following code defines a predicate At with an argument named l of type Location and an implicit argument named tau of type Robot. The associated rule enforces that a robot cannot go on a location outside of the first quadrant of the Cartesian space.

class Robot {

  predicate At(Location l) {
    l.x >= 0;
    l.y >= 0;
  }
}

A similar result can be achieved by defining a predicate through

predicate At(Robot tau, Location l) {
  l.x >= 0;
  l.y >= 0;
}

The language does not allow the definition of predicates having the same identifier within the same class. We will see soon how disjunctions can be explicitly defined within the body of the rules.