Specifying argument types for abducible (Experimental)

The current abductive system allows non-ground abducible to be assumed/collected during the inference. The variables in a collected abducible may be bound to some term after the system solve other goal later, or they may remain in the abducible in the final answers. In many cases, we may want to specify the types of an abducible predicate's arguments, in order to further restrict what abducibles can be collected. One way of achieving this is through integrity constraints. For example,

action(goto(X)) :- place(X).
action(buy(I, X)) :- item(I), place(X).

ic :- happens(E, T), \+ action(E).

However, in the above approach, the type checking of an abducible's arguments is still performed after the abducible is collected. Fortunately, the abductive system provides a way to force the type checking to be done before the abducible is collected, if it is desired. This is done by giving the abducible argument types in the abductive theory, which contains the following parts:

• a specific domain has a name (as constant) and a list of members (as constants), is declared using enum(DomainName, ListOfDomainMembers).
• the argument types of an abducible are declared using types(Abducible, ListOfConditions), where Abducible is an abducible predicate with all the arguments being variables, and ListOfConditions is a list of type conditions being either Var = Term or type(Var, DomainName).

For example, in the shopping trips planning problem, if we know in advance that there are only two possible actions (i.e., goto and buy), and we also know their argument types, then we can add the following abducible argument type declarations in the abductive theory:

enum(place, [hws, sm]).                        
enum(item, [drill, milk, banana]).
           
types(happens(E, T), [
    E = goto(X),
    type(X, place)                                   
  ]).
types(happens(E, T), [
    E = buy(X, Y),
    type(X, item),
    type(Y, place)     
  ]).

Note that in types/2, some of the arguments of the abducible may still be un-typed, e.g. T. Note also that there may be multiple types/2 definitions (i.e., argument type specifications) of the same abducibles, which means the arguments of the abducible must satisfy at least one of the specifications.

With these specifications, the abductive system behaves as follows when an abducible is collected:

• if there is a type specification for the abducible, the system will check the already ground arguments of the abducible against the specification, and will ground as many variable arguments in the abducible as possible according to the specification.
• if there is no type specification for the abducible, the system does not perform any argument type checking.

This feature has two advantages: (1) in some problem domains the query computation may be speeded up (significantly), and (2) the abductive theory may be simplified. For example, with the abducible argument type specifications, some of the action effect conditions

initiates(goto(X), at(X), T) :- place(X).
terminates(goto(X), at(Y), T) :- place(X), place(Y), X =/= Y.

can be simplified to be

initiates(goto(X), at(X), T).
terminates(goto(X), at(Y), T) :- X =/= Y.