A Parameterised Module System for Constructing Typed Logic Programs

1 Introduction

Logic programming has been used extensively for representing and reasoning about knowledge bases. For large knowledge bases we require a means of segmenting the program so that small component parts of the knowledge base can be developed. These can then be used to build larger components, and so on, until the program is completed. These components are called modules.

Modules can be researched from a number of points of view including software engineering, object-oriented programming, and theory con­ struction. We concentrate here on the software engineering use of modules and, in particular, the use of modules in program construction. There are a number of requirements for such a module system.

1. There must be a means of combining mod­ ules. This is normally achieved by allowing one module to import another.
2. Part of a module should be protected from unintended use by other modules. This is called encapsulation. Usually a module is divided into two parts. One part defines a language that can be used by an importing

·supported by SERC grant GR/H/79862

module. The other part extends this lan­ guage with symbols only required locally.

1. It should be possible to develop a mod­ ule independently of other modules that it does not import. Thus the import relation is normally restricted to defining a partial order on the modules in a program. The order of compilation of the modules must then respect this ordering.
2. A module should be usable in as many con­ texts as possible. A module providing an abstract data type such as a stack or a def­ inition of an abstract relation such as tran­ sitivity needs to be re-usable and not tied to a specific application.

The reasons for having types in logic program­ ming languages are well known. The struc­ ture of the knowledge domain can be repre­ sented directly by means of type declarations. These declarations also define the intended use of the symbols and therefore protect the pro­ gram from syntactic errors caused by misuse of the symbols. The language on which we have based our ideas is the logic programming language Godel [Hill and Lloyd, 1992]. Godel has a parameterised type system that supports generic but not inclusion polymorphism. More­ over, Godel has a simple module system that supports importation, encapsulation, and sepa­ rate compilation as well as allowing for modules defining abstract data types. The Godel mod­ ule system does not support re-usable modules defining abstract relations such as transitivity. The parameterised module system described here extends the module system in Godel so as to provide better facilities for defining abstract relations in re-usable modules.

Other authors have investigated modules for logic programming. [Miller, 1986] extends Pro­ Jog to provide a theory of modules over Horn clauses. The modules are defined by nested im­ plication with the semantics based on intuition­ istic logic. In this module system, the modules are dynamic in the sense that they are created

and deleted at run time. Thus a modification of SLDNF-resolution is required for the procedural semantics.

The module system given in [O'Keefe, 1985] only deals with untyped programs where the predicates are considered to be local to the modules but the functions are assumed to be global. Thus abstract data types cannot be defined. A number of Prolog implementations supporting module systems similar to that de­ scribed by O'Keefe have been marketed.

[Sannella and Wallen, 1992] describe a Prolog module system based on the theory of modu­ larity underlying the Standard ML module sys­ tem. This module system (extended to include types) provides all the facilities provided by Godel. It also allows for a form of parame­ terised modules although the parameterisation is with respect to the module names instead of the symbols. However, the main difference is that a predicate must be defined in a sin­ gle module, whereas, in our system, predicates that are parameterised can be defined in more than one module. The system is less flexible than the one described here but safer in that the predicates are better protected from unin­ tended use.

[Goguen and Meseguer, 1984] present EqLog which combines functional and logic program­ ming. The language provides a parameterised module system which appears to be similar in function to the module system described in [Sannella and Wallen, 1992]. However, it is described in the framework of EqLog rather than Prolog so that it is not immediately ap­ plicable to logic programming languages.

[Antoniou and Sperschneider, 1992] divide a module into four parts; import, export, body, and parameter. The import and export parts use Horn Clauses to specify the imported and exported predicates. These are only used for the combination of the modules. Exported predicates are also defined in the body part of the module. It is these definitions that are used in the execution of the program. The pa­ rameter part specifies generic predicates using full first order logic. Importing modules sup­ ply the implementation for each of these pred­ icates. This must be correct with respect to its specification. Since each module has to de­ note a complete theory, every predicate in the module must be completely defined within the module. This disallows the more flexible sys­ tem described in the current paper.

The paper 1 is organised as follows. In the next section, Godel's module system is explained. We show how this can be extended to include parameterised modules. In section 3, we give a number of definitions associated with a module­ free typed logic program which are needed later. Then, in section 4, we provide a formal definition of a modular program with parame­ terised modules. Finally, section 5 outlines the intended semantics for such a program.

1 A version of this paper with several longer examples showing the use of parameterised modules is available as a technical report. [Hill, 1993]

2 The Godel Language

The module system in Godel is best explained by means of an example 2 ·

EXPORT TheJonesFamily.

BASE

Person.

COISTAIT Eve,Pat,Bob,Tim,Mary: Person.

PREDICATE Mother,Father: Person·Person.

LOCAL

TheJonesFamily.

Father(Bob,Pat).

Mother(Pat,Mary).

EXPORT TheJonesRels.

IMPORT TheJonesFamily.

PREDICATE Anc: Person · Person.

LOCAL TheJonesRela.

PREDICATE Par: Person · Person.

Par(x,y) <- Mother(x,y) \/ Father(x,y).

Anc(x,y) <- Par(x,z) t Anc(z,y).

Anc(x,y) <- Par(x,y).

In both of the above modules there are a num­ ber of declarations and statements. The state­ ments are formulas in the language defined by the declarations. There are two kinds of dec­ laration: language and module. The language declarations begin with a key word that indi­ cates the category 3 of symbol being declared. In TheJonesFamily module, Person is declared to be a base type; Eve, Pat, etc., are declared to be constants of type Person; Mother and Father are declared to be predicates with ar­ guments of type Person. In Godel, a symbol name (for a given arity and category) must have at most one declaration in a module.

Each module is in two parts called export and local. A part begins with a module declara­ tion stating whether it is the export or local part and the name of the module. The export part contains language declarations for symbols that can be used in this module and also in other modules that import it. Thus the type Person can be used in TheJonesRela as well as in either part of TheJonesFamily. Symbols declared in the local part of a module are only available for use within this part. Hence, since TheJonesRels declares Par in the local part, Par cannot be used outside this module. State­ ments are only allowed in the local part of a module. These define the predicates declared in either part of the module. TheJonesRels also has a module declaration that begins with the key word IMPORT. This makes all the symbols declared in the export part ofTheJonesFamily available for use in TheJonesRels.

lpar, Rela, Anc are short for Parent, Relation~, Ance&tor.

3 The categories are: type constructor, function, or predi­ cate. A base, constant, or proposition is regarded as a con­ structor, function, or predicate, respectively, of arity 0.

The example illustrates the many-sorted types in Godel. However, in Godel, we can also de­ fine generic functions and predicates. A com­ mon example of such a data structure is a list, which is defined to be a list of terms of a cer­ tain type, but the particular type to be used is not specified. For example, Godel provides a system module Lists. This module exports the type constructor List, constant Mil, func­ tion Cons, and predicate Member with language declarations:

COISTRUCTOR List/1.

COISTAIT lil: List(a).

_

FUICTIOI Cons: a·List(a)->List(a).

PREDICATE Member: a·List(a).

If the language included the base type Int, then we have the types List (a), List (List (a)), List(Int), List(List(Int)), etc. The tu­ ples of types in a declaration is called a de­ clared type. Other types for lil, Cons, and Member can be obtained from their de­ clared types by means of type substitu­ tions. Thus lil also has types List(Int) and List(List(Int)), Cons has types Int · List(Int) -> List(Int) and List(Int) · List(List(Int)) -> List(List(Int)), and Member has types Int · List(Int) and List(Int) · List(List(Int)).

A definition of a constructor C is a set of func­ tion declarations with range type of the form C{tl> ... , tn) (or C, if the arity n is 0). A def­ inition of a predicate P is a set of statements with P in the head.

A Go del program for a module m (called the main module) is the smallest set of modules that includes m and is closed wrt the mod­ ules named in the import declarations. The program must satisfy the following three con­ ditions.

• Ml The module names can be partially or­ dered so that if m' occurs in an import declaration in a module named m then m' <m.
• M2 Every symbol appearing in (the export part of) a module, must be declared in or imported into (the export part of) the module.
• M3 Each constructor or predicate with a non­ empty definition in a module must be de­ clared in that module.

These conditions enable independent com­ pilation and protect procedures defined in one module from being modified by another. The set of modules {TheJonesFamily, TheJonesRels} form a Godel program.

In the example, a module containing general rules about family relations was forced, by the module system, to contain a declaration im­ porting a module defining a specific family thereby preventing its reuse with other fami­ lies. Thus we propose to modify the above lan­ guage to allow parameterised modules. In the next example, a Rels module is parameterised wrt the base Person and predicates Mother and Father. Note that, here it is the TheJones module that imports the Rels module, whereas in the previous example, the importation was in the opposite direction.

EXPORT TheJones.

IMPORT Rels(Jones,Ma,Pa).

BASE

Jones.

PREDICATE Ma,Pa: Jones · Jones.

COISTAIT Eve,Pat,Bob,Tim,Mary: Jones.

LOCAL

TheJones.

Pa(Bob,Pat).

Ma(Pat,Mary).

EXPORT Rels(Person,Mother,Father).

BASE

Person.

PREDICATE Mother,Father: Person·Person.

PREDICATE Anc: Person * Person.

LOCAL Rels(Person,Mother,Father).

IMPORT Trans(Person, Par).

PREDICATE Par: Person · Person.

Par(x,y) <- Mother(x,y)\/Father(x,y).

Anc(x,y) <- Tr(x,y).

EXPORT Trans(Point,Connect).

BASE

Point.

PREDICATE Connect: Point · Point.

PREDICATE Tr: Point · Point.

LOCAL Trans(Point, Connect).

Tr(x,y) <- Connect(x,y).

Tr(x,y) <- Connect(x,z) t Tr(z,y).

The module name that follows the key words EXPORT and LOCAL consists of an identifier with 0 or more symbols as arguments. The set of declarations for these symbols (which must be in the export part of the module) is called the signature of the module. For exam­ ple, Rels (Person, Mother, Father) is a mod­ ule name with identifier Rels and signature

BASE Person.

PREDICATE Mother,Father: Person·Person. Symbols that are declared in a module but are not in the signature are said to be completely specified by the module. For example, the base Jones is completely specified in TheJones.

The written module is the initial module. In­ stances of these modules can be obtained by substituting new symbols for symbols occur­ ring in the module name. The substituted sym­ bols must be distinct from symbols completely specified by the initial module. Thus the fol­ lowing module is imported into Rels (Person, Mother, Father).

EXPORT Trans(Person,Par).

BASE

Person.

PREDICATE Par: Person · Person.

PREDICATE Tr: Person · Person.

LOCAL Trans(Person,Par).

Tr(x,y) <- Par(x,y).

Tr(x,y) <- Par(x,z) t Tr(z,y).

Note that if a symbol is completely speci­ fied in a module it is completely specified in every module that is an instance of this module. Thus the predicate Tr is com­ pletely specified by Trans (Point, Connect) and Trans (Person, Par) . (Trans (Person, Tr) could not occur in an import declaration in a module since Tr is completely specified in Trans (Person, Connect).)

We define a modular program in a similar way to the definition of a Godel program above. In­ formally, it is a set of initial modules with a main module, closed wrt the identifiers in the import declarations and satisfying similar mod­ ule conditions to those given above.

Ml* The identifiers in the module names can be partially ordered so that if I' is an identi­ fier in an import declaration in a module with identifier I then I' < I .

M2* Every symbol name appearing in (the ex­ port part of) a module m, must either be declared in (the export part of) m or be completely specified by the export part of a module that is imported into (the export part of) m.

M3* Each constructor 'or predicate name de­ clared in or imported into a module and completely specified by an imported mod­ ule n may only have a non-empty definition in n or in imported modules that are also imported into n.

The set of mo'dules

{TheJones,

Rels(Person,Mother,Father),

Trans(Point,Connect)},

together form a modular program for the The Jones .

The previous example shows the way the mod­ ule system works where each module imports no more than one module and each of the con­ structors and predicates is completely defined within a module. However, the parameterised module system allows for multiple inheritance and also for a predicate or constructor defini­ tion to be split between several modules. To illustrate this, we define another family named Hill. Due to marriage between the families, we create a new family with name HillJones.

EXPORT

BASE

TheHillJones(HillJones,Ma,Pa).

HillJones.

PREDICATE Ma,Pa: HillJones · HillJones .

IMPORT TheJones(HillJones,Ma,Pa),

TheHills(HillJones,Ma,Pa).

COISTAIT Pam: BillJones.

LOCAL TheHillJones(HillJones,Ma,Pa).

Ma(Mary,Pam).

Pa(Tom,Pam).

EXPORT TheHills(Hill,Ma,Pa).

BASE Hill .

PREDICATE Ma,Pa: Hill · Hill.

IMPORT Rels(Hill,Ma,Pa).

COISTAIT Robin,Jill,Tom: Hill.

LOCAL TheHills(Hill,Ma,Pa) .

Pa(Robin,Tom).

The set of modules

{TheHillJones(HillJones,Ma,Pa),

TheHills(Hills,Ma,Pa),

TheJones(Jones,Ma,Pa),

Rels(Person,Mother,Father),

Trans(Point,Connect)}

forms the modular program with main module TheHillJones. A goal for the program is

<- Anc(Bob,x) t Anc(Robin,x).

3 Typed Logic Programs

The Godellanguage is based on typed first or­ der logic, where each non-logical symbol has a language declaration. This associates the sym­ bol with a tuple of symbols in another language, called the type language.

In a type language for a parametric type system as used in Godel, the types are structured ex­ pressions defined over disjoint sets of construc­ tors and parameters. Each constructor has an arity associated with it. Thus the constructor declaration C / n ( n ~ 0) assigns the arity n to a constructor C. A type in the type language T defined over a set of constructor declarations C is defined recursively, to be either a parame­ ter or of the form C(t1, ... , tn) , where C/n E C and t1, ··· ,tn are types in T .

Since, in this paper, we need to define type lan­ guages in a modular program, we must have a means of constructing a new type language from a set of existing type languages. Let T, 7i, ... , 7i be type languages defined over the sets of constructor declarations C, C1, . .. , C~:, respectively, using the same set of parameters. Then we say that T is the join of the set {7i, . .. , T~:} if C = Ct u · · · u C~:. If Co is a set of constructors and T' a type language de­ fined on the set CUCo, then T' is the extension ofT using Co.

A first order typed language C based on a type language T consists of a set of formulas, where the formulas are defined wrt a set of function declarations :F over T, a set of predicate decla­ rations P over T, and a set of variables V.

The function declaration F : T1 * · · · * Tn - T assigns a nonempty tuple of types T1, ... , Tn, T called the declared type to a function F of ar­ ity n. It is assumed that every parameter in the tuple occurs in the last type. The set of functions in :F must be disjoint from the set of variables V.

The predicate declaration P : r 1 * · · ·*Tn assigns a tuple of types ( Tt, . .. , Tn) called the declared type to a predicate P of arity n.

If e is a type substitution, the function F also has the type (rl 9, ... , Tn9, T9), range type T9, and domain type (rl e, ... , Tn9) . Similarly, the predicate p has type ( T1 9, ... , Tn9).

Using sets of function and predicate declara­ tions :F and P and a set of assignments of types to variables, called a variable typing, we define a term with its associated type and an atom.

1. A variable x is a term whose type is as­ signed to x by the variable typing.
2. If a function F has type ( r1, ... , Tn, T) and A1, ... , An are terms of types T1, ... , Tn, then F(At, ... , An) is a term of type T.
3. If a predicate P has type ( T1 , ... , Tn) and A1. ... , An are terms of types T1, ... , Tn, then P(A1, ... , An) is an atom.

It is now straightforward to define a formula in C (see [Hill and Topor, 1992]).

Language declarations with the same category and arity in C are similar. If each symbol has a unique declared type, then C is universal. In this paper we assume that all the languages are universal. Since the category and arity can be used to distinguish symbols with the same name, we require similar declarations that are not identical to have distinct symbol names.

For each i E {1, ... , k }, let C; be a first order typed language defined wrt the sets of function and predicate declarations :F; and 'P;. Suppose also that C is a first order language defined wrt the sets of function and predicate declarations :F and 'P. Then Cis the join of {£1, .. . , Ck} if :F = :F1 U · · · U :Fk and P :::::: 'P1 U · · · U 'Pk. If :Fo and 'Po are sets of function and predicate dec­ larations, and C' a first order language defined wrt :FoU:F and 'PoU'P, then C' is the extension of C using :Fo and 'Po.

Let C be a universal first order language de­ fined wrt the sets :F and P of function and predicate declarations and P : r 1 * ... * Tn a predicate declaration in P. A statement for P

is a formula inC of the form P(A1, ... , An} or P(A1, ... , An) <- W with some assignment V of types to the variables in the statement, where W is a formula and At, ... , An are terms of type Tl, ... ,Tn using :F and V. P(Al, ... ,An) is called the head of the statement.

A module-free program IT consists of a set of language declarations defining a type language T (called the type language of IT), a typed first order language C based on T (called the lan­ guage of IT), and a set of statements in C. A goal G for IT is either the empty clause or of the form <- W where W is a formula in the language of IT.

The declarative semantics of a module-free (typed) logic program is based on a typed form of the Clark completion of logic programs us­ ing an equality predicate that has declared type (a, a) where a is a parameter. Details can be found in [Hill, 1992] and [Hill and Topor, 1992].

4 A Modular Program:

Definition

We now define a module JJ(m)' 4 and a modular program ITm with main module m 4 .

We first define a simple module m which is a module with no import declarations and has import depth 0. It consists of a set { m, Exp, Loc} where m is the name of the module, The name m consists of an identifier followed by 0 or more symbols. These sym­ bols must have their constructor Cm, function :Fm, and predicate 'Pm declarations in Exp. The set Cm U :Fm U 'Pm is called the signa­ ture of m. Exp = {0, cE~p. :FE~p. 'PE~p}, and Loc = {0, CLoc, :FLoc, 'PLoc, S}. Exp is the ex­ port part and Loc is the local part for m . . CE~p and CLoc are disjoint sets of constructor decla­ rations. CE~p- Cm defines the export type lan­ guage for m and CEzp U CLoc (resp., CEzp) de­ fines the type language form (resp., export part of m). :FEzp and 'PEzp are sets of function and predicate declarations in the type language for the export part of m. :FLoc and 'PLoc are sets of function and predicate declarations in the type language for m. :FEzp- :Fm and 'PEzp- 'Pm define the export language. :F Ezp U :FLoc and 'PEzpU'PLoc define the language form (which is assumed to be universal). Sis a set of program statements in the language for m. A symbol 8 with a declaration in m is completely specified by m if 8 does not occur in the name m.

The module, as written is called an initial sim­ ple module. Instances of initial modules can be obtained by means of module substitutions. A module substitution 8 for a module m is a substitution whose domain is a subset of the symbols in m and whose range is any set of names not completely specified by m. This set must be such that JJ(m)8 is a (simple) module. In particular, the language for JJ(m)8 must be universal. Thus, if symbols St and s2 have sim­ ilar declarations dt and d2, respectively, in m and 8t8 = 828, then dt8 and d28 must be the same.

·we use the module name m instead of p(m) if it is clear from the context which module the name m is referring to.

The modular program 11m for m is the singleton set {JJ(m)}.

Suppose we have a set ~ of initial modules with distinct module identifiers such that, for each module i E ~. a modular program II; for i is in ~ and the import depth of i is < d. A module m is a set {m, Exp, Loc} where Exp = {IE~p.CE~p. :FE~p· PE~p}, and Loc = {hoc.CLoc. :FLoc. 1'Loc. S}. The name m consists of an identifier not in~ followed by 0 or more symbols. These symbols must have their constructor Cm, function :Fm, and predicate Pm declarations in Exp. The set Cm U :Fm U Pm is called the signature of m. Exp is the export part and Loc is the local part for m. Ie~p and hoc are sets of module names. Every symbol in IE~p (resp., hoc) that is not completely speci­ fied by an imported module should have a lan­ guage declaration in Exp (resp., Exp U Loc). For each i E I= IE~p U hoc, there must be a (unique) module JJ(i') in ~and a module sub­ stitution 8; such that i = i' 8; and JJ( i')8; is a module (denoted by JJ(i)). The import depth of m is one more than the maximum of the im­ port depths of modules JJ(i) where i E / . We say that a module i is available to m (resp., the export part of m) if either i = m or there is a modulej E I (resp., j E lE~p) and i is available to the export part of j.

CE~p and CLoc are disjoint sets of constructor declarations. Let T 1 (resp., Tl~p) be the join of the export type languages for i, i E I (resp., i E IE~p ). The export type language for m is the extension ofTl~P using CE~p-Cm . The type language form (resp., the export part of m) is the extension of T 1 using CE~p U CLoc (resp., CE~p)· :FE~p and PE~p are sets of function and predicate declarations in the type language for the export part of m. :FLoc and 1'Loc are sets of function and predicate declarations in the type language for m. Let C/ (resp., .C~~p) be the join of the export languages for i, i E I (resp., i E IE~p)· The export language for m is the extension of .C~~P using :F E~p - :Fm and PE~p - Pm and the language for m is the ex­ tension of .C 1 using :F E:&p U :FLoc, 1' E~p U 1' Loc. The language for m must be universal. Thus, if module i is available to m and a symbol s has similar declarations d in m and d; in i, then d and d; must be the same. Similarly, if modules i and j are available to a module and a symbol 8 has similar declarations d; in i and d; in j, then d; and d; must be the same. Finally, the set S is a set of statements in the language for m such that every predicate in the head has a declaration in PE~p U 1'Loc·

We say that a symbol 8 is completely specified by m if 8 does not occur in m and there is a language declaration for 8 in JJ(m).

The module as written is called the initial mod­ ule. Instances of initial modules can be ob­ tained, as for simple modules, by means of module substitutions.

The program 11m is the union of {JJ(m)} with the union of the programs II;,, for each initial module i' in ~ such that, for some module sub­ stitution 8, i = i'8 and i E I. The language of 11m is that of m.

5 A Modular Program: Semantics

In this section we define a mapping called a de­ modularisation from a modular program to a module-free program. The semantics of a mod­ ular program is then defined to be the seman­ tics of its demodularisation.

A symbol, declared in or imported into an ini­ tial module m, is assumed to be distinct from any other symbol that is completely specified in an imported module. If the programming lan­ guage (such as Godel) allows overloading, then the overloaded names of distinct symbols de­ clared or imported into the initial module must be standardised apart before the demodularisa­ tion mapping is applied.

The two components of a demodularisation are the generating of imported modules from initial modules and the standardising apart of names in the local parts of the imported modules. The demodularisation of a module is defined by in­ duction on its import depth.

We first define an associated simple module u( m) for a modular program 11m for an ini­ tial module JJ(m) by induction on its import depth. It is assumed that the character'!' does not occur within the declared symbols.

1. If JJ(m) is an simple module, then JJ(m) is
2. the associated simple module for 11m.
3. Suppose JJ(m) has import depth > 0. For each initial module JJ(i') such that, for some module substitution 8, i = i'8 occurs in an import declaration in JJ(m), obtain the associated simple module u(i').
4. For each module name i in an import dec­ laration in (the export part of) JJ(m) con­ struct an imported simple module for (the export part of) JJ(m) as follows. If i' is an initial module name and 8 is a module sub­ stitution such that i = i' 8, let u( i) denote u(i')8. Then, for each symbol 8 in u(i),

if a module j is available to p( i) but not available to the export part of p( i) and s is completely specified by j, replace each occurrence of s in u( i) by j!s.

1. Let u(m) be the module with name and signature of the module p( m) and contain­ ing all the language declarations and state­ ments in p(m) together with all the lan­ guage declarations and statements in the imported simple modules for m. The ex­ port part of u( m) contains all the declara­ tions in the export part of p( m) and the export parts of the imported simple mod­ ules for the export part of p(m).

The demodularised program for the modular program llm is the program obtained from u(m) by removing the module declarations and combining the local and export parts.

It can be shown that p(m) together with its imported simple modules is a modular program of import depth 1 and u( m) is a simple module whose language is the same as that of llm.

We illustrate the demodularisation using the modular program for TheJones in section 2. First we give the associated simple module u(Rels(Person, Mother, Father)) .

The imported simple module Rels(Jones, Ma, Pa) for TheJones is obtained by apply­ ing the module substitution {Person/ Jones, Mother/Ma, Father/Pa} to the above module and then replacing each occurrence of Par by Rels(Jones,Ma,Pa) !Par. We conclude the pa­ per with the demodularisation of the modular program with main module TheJones.

Rels(Jones,Ma,Pa)!Par(x,y) <­ Ma(x,y) \/ Pa(x,y).

Anc(x,y) <­

Trans(Jones,Rels(Jones,Ma,Pa)!Par)! Tr(x,y).

Trans(Jones,Rels(Jones,Ma,Pa)!Par)! Tr(x,y) <­

Rels(Jones,Ma,Pa)!Par(x,z) ~ Trans(Jones,Rels(Jones,Ma,Pa)!Par)! Tr(z,y).

Trans(Jones,Rels(Jones,Ma,Pa)!Par)! Tr(x,y) <­

Rels(Jones,Ma,Pa)!Par(x,y) .