Facts and goals

Once defined predicates and rules, we can now show how to describe facts and goals for our problems. Still following the object-oriented paradigm, we consider facts and goals as objects and, as such, we will create them through the new operator. However, since, unlike other languages, we have no means to distinguish facts and goals, we have to distinguish them explicitly through the keywords fact and goal as a prefix of the identifier. Suppose, for example, we want to express the fact that our agent is at some location, we might use the following statement:

fact at_0 = new At();

We can now address the arguments of the fact just as if they are members of the object represented by at_0. So we can, for example, put constraints on the coordinates of the locations.

at_0.l.x <= 10;

It is worth to note that creating a fact or a goal will, unless specified, create existentially scoped variables for each of its arguments. As a result, the same rule valid for existentially scoped variables, stating that at least one instance of the type must have been previously created, applies also to the creation of facts and goals. Executing the previous example, without previously creating instances of locations, would result in an inconsistent problem and, therefore, the solver would have returned $\bot$.

A convenient method to avoid the creation of existentially scoped variables is to explicitly state the allowed values for an argument. This can be achieved by making use of the syntax <id>:<expr>, where <id> represents the identifier of an argument and <expr> is an expression, within the parenthesis of the new fact or goal. For example

Location l0 = new Location();
fact at_0 = new At(l:l0);

creates a new location l0 and a new fact at_0 whose parameter l assumes the value l0;

In order to better understand, let us consider a complete example:

// we define a Location class
class Location {

  real x;
  real y;

  Location(real x, real y) : x(x), y(y) {}
}

// we define a predicate At
predicate At(Location l) {
  l.x >= 0;
  l.y >= 0;
}

// we create three instances of location
Location l0 = new Location(0, 0);
Location l1 = new Location(1, 1);
Location l2 = new Location(2, 2);

// we create an At fact
fact at_0 = new At();

// we add some constraints on the fact
at_0.l.x <= 1;
at_0.l != l0;

// we create an At goal specifying its l parameter
goal at_1 = new At(l:l2);

It is worth to note that both facts and goals can be created within the body of a rule. This allows us to define subgoals for the reasoning process. Suppose, for example, we want to express the fact that "All men are mortal", we might use the following rule:

predicate Mortal (Thing x) {
  goal m = new Man(x:x);
}

The creation of scoped formulas (i.e. formulas with a tau parameter), either facts or goals, follows a similar syntax. However it is required that the scope is explicitly specified. This can be achieved through the following syntax:

[fact | goal] <id> = new <qualified_id>.<id>(<id>:<expr>, <id>:<expr>, ...);

where <qualified_id> identifies the scope. The following code, for example, creates two robots and two facts having a different values for their respective tau parameters.

Robot r0 = new Robot();
Robot r1 = new Robot();

fact f0 = new r0.At(l:l0);
fact f1 = new r1.At(l:l1);

Note that the tau argument of the fact f0 is constituted by an object variable whose domain contains the sole robot r0. Similarly, the tau argument of the fact f1 is constituted by an object variable whose domain contains the sole robot r1.

It is worth to notice that nothing prevents to create facts and goals having existentially scoped variables as tau argument. As an example

Robot r0 = new Robot();
Robot r1 = new Robot();

// we create the existential variable
Robot r;

goal g = new r.At(l:l0);

creates a goal g whose tau has, as allowed values, the two robots r0 and r1 (i.e. its allowed values is constituted by the set {r0, r1}). This syntax allows the possibility to leave to the solver the responsibility to decide which robot should achieve the l0 goal.

Finally, in case facts and goals are created within a rule, their scope is inherited from the rule. Suppose, for example, the following rule stating that, in order for a given robot to stay at a given location, the robot must go to that location, the scope of the $gt$ goal will be the same of the one that required the application of the rule. Similarly to the above example, the following code leaves to the solver the responsibility to decide which robot should achieve the l0 goal however, whatever the chosen robot, the same robot will also require to go to the same location.

class Robot {

  predicate At(Location l) {
    goal gt = new GoTo(l:l);
  }
}

Robot r0 = new Robot();
Robot r1 = new Robot();
Robot r;

goal g = new r.At(l:l0);