Organization of theory based systems

Abstract

A method of controlling the operation of a computer database system. The method of the invention is particularly adapted for use in processing a query in a computer system which has an inference engine, query processing means, and a set of object theories and metatheories. The method includes providing a system theory to define coupling relationships between the object theories and metatheories, selecting an object theory and associated metatheories according to the system theory in dependence on parameters of a query to be processed, and processing the query by the theories so chosen. The coupling relationship may be an interpreter, an assimilator or an attribute metatheory.

Claims

What is claimed is:

1. A method of controlling the operation of a computer database system in processing a query, the system being of the kind that has an inference engine, query processing means, and a plurality of metatheories, the method comprising:

providing a knowledge base;

logically partitioning the knowledge base into a plurality of object theories;

providing a system theory that defines many-to-many coupling relationships between the object theories and a plurality of the metatheories including an interpreter metatheory;

selecting an object theory and associated metatheories according to the system theory in dependence on parameters of a query to be processed; and

processing the query by the theories so chosen.

2. A method according to claim 1 wherein the step of providing a system theory comprises providing a system theory that defines a coupling relationship between the object theories and an assimilator metatheory.

3. A method according to claim 1 wherein the step of providing a system theory comprises providing a system theory that defines a coupling relationship between the object theories and an attribute metatheory.

4. A method according to claim 1 wherein a coupling relationship is expressed as a clause of first-order logic and wherein the system theory includes a declarative model that provides an explicit description of querying and updating within the system.

Description

The present invention relates to the organization of theory-based systems and, more particularly, to the organization of a logic programming system or knowledge representation and management system based on logic programming, which incorporates a provability interface to multiple modules, databases or theories.

The basic terms such as theory, metatheory, assimilation, and provability used in this specification follow the usage of D. A. Bowen and R. A. Kowalski, "Amalgamating Language and Metalanguage in Logic Programming", pages 153-182 of Logic Programming, edited by K. L. Clark and S. A. Ternlund, Academic Press, New York, 1982 and also K. A. Bowen and T. Weinberg, "A Meta-level Extension of Prolog", pages 48-53 or 1985 Symposium on Logic Programming, Boston, IEEE. It is to be understood that the term "theory" as used herein encompasses equivalent concepts such as logic databases, modules and worlds (the latter term being one used by H. Kauffmann and A. Grumbach in "Representing and Manipulation Knowledge within Worlds", at pages 61-73 of Proc First Int Conf on Expert Database Systems, Edited by L. Kershberg, 1986).

The present specification also assumes a basic knowledge of logic programming such as that possessed by any skilled worker in the field. In particular, some knowledge of the logic programming language Prolog is assumed. For a basic text, refer to "Programming in Prolog", W. F. Clocksin and C. S. Mellish, Springer-Verlag, 1984). Another very useful reference is the paper by R. A. Kowalski entitled `Problems and Promises of Computational Logic` published as part of the Computational Logic Symposium Proceedings, Brussels, November 1990 and edited by J. W. Lloyd. The basic concepts of a knowledge-base management system are also assumed (see Proc First Int Conf on Expert Database Systems, cited above).

Rather than having a homogeneous knowledge base, in practice, some kind of partitioning of the facts and rules of a knowledge base system is often desirable for various reasons some examples of which are:

modularization of knowledge can reflect the conceptual structuring of a problem,

it permits the existence of mutually inconsistent theories:

a partition of the knowledge base can be treated as an `object` for purposes of metaprogramming--specialized inference control and specialized assimilation control can be particularized to certain partitions. Those partitions can be subjected to more than one regime of control;

it is the primary mechanism through which scale is controlled. Partitions are not affected by the growth of other partitions as they might be with flat knowledge bases; theories become a code module structure (theories can be reused in more than one application);

the partitioning of knowledge in theories enables different theories to be realized in foreign systems where desirable. For example one theory which appears to be a large set of ground structureless facts might in reality be stored in a relational database and managed by a relational database management system.

The simplest form of partitioning is to divide the system into entirely independent theories. However, this effectively results in a number of entirely independent modules, which is of very little use. A more useful form of partitioning involves modularising the knowledge base into distinct subsystems, but preserving some form of coupling between those subsystems.

Two main types of partitioning are possible.

If the functionality of a theory is considered in detail, it will be realized that several reasonably distinct areas of functionality can be distinguished. These functionalities can be partitioned out from the basic theory as metatheories; theories which are concerned with the basic theory as an object or operand.

One function of the basic theory is the inbuilt reasoning or interpretation function, but in some circumstances it may be desirable to provide an additional and more elaborate interpreter function. If it is desired to be able to update the theory, then assimilator means are required with the functionality for ensuring the updates do not introduce inconsistency. Further, the updating may involve checking against factual data to ensure, for example, that various values are within appropriate ranges, and the range information may be regarded as attribute information distinct from the functionality of assimilation, requiring an attribute function.

Thus it may be desirable to have a number of metatheories, performing different specialized functions, associated with a given theory. The present system provides for three types of metatheory--interpreter, assimilator and attribute metatheories.

The use of such metatheories and the sharing of metatheories between object theories is known e.g. from the Bowen and Weinberg paper mentioned in the introduction of this application.

Another type of partitioning is the partitioning of the basic or main theory into different subject matters, giving a set of theories, all on the same "level", which we can conveniently describe as object theories.

Although these two types of partitioning are logically distinct, it is advantageous to use them in combination. This permits the sharing of a single metatheory by several object theories, whereas partitioning of object theories alone would require the same metatheory statements and rules to appear in several object theories.

FIG. 1 of the accompanying drawings illustrates known types of partitioning by showing a fragment of a hypothetical system containing a variety of different theories and the relationships between them. The principal forms of relationship are illustrated in this example, which gives the flavour of a relational database application.

The theory-metatheory relationships are of three different kinds, of a theory with its interpreter, assimilator, and attribute metatheories; these are indicated by the different types of line indicated as I, As, and At respectively.

Three object theories 20 to 22--an employment theory 20, a parts theory 21, and a suppliers theory 22--are together equivalent to a typical database of primarily factual data. The employment theory 20 is primarily a collection of facts concerning various people; it includes their employment details and also various simple relationships between them (such as spouse and parent-child relationships). The parts theory 21 is primarily a collection of facts about parts and components for a factory and the suppliers theory 22 is primarily a collection of facts about the suppliers of various raw materials for the factory.

The parts theory 21 and the suppliers theory 22 are both inherently factlike and so each can have an interpreter which takes account of this and performs fact look-up instead of full theorem proving. These two theories therefore have a common interpreter 26. In the same way, they have a common assimilator 27, which ensures that the individual theories remain semantically consistent. This therefore illustrates two of the three types of theory-metatheory relationship and a metatheory being used by two different object theories.

The employment theory 20 has an interpreter theory 23, an assimilator theory 24 and an attribute theory 25. The employment theory may include certain rules in addition to factual statements, so its interpreter 23 must incorporate a full theorem prover. The assimilator theory 24 is a specialized assimilator which ensures that any new data added to the employment theory does not violate any specified constraints.

One type of constraint concerns the nature of the data being added; for instance, it must be consistent with a group of data, such as employee grade data, that is allowed in that theory. The allowed groups of data are defined in the attribute theory 25, which contains all the metadata about the employment theory. Thus to perform this check, the assimilator needs to reference (prove a result) in the attribute theory. Thus the metatheory level need not be flat; a metatheory can be manipulated by a further metalevel which is a "metametatheory" to the original object theory and simultaneously a metatheory to the original metatheory.

In addition to the three fact-like theories 20 to 22, there is a genealogy object theory 28, which is primarily composed of a set of rules defining complex genealogical relationships, such as ancestorhood and cousinhood and many of which are therefore recursive. This theory has a special interpreter theory 29, which is designed to deal efficiently with recursive rules and so restrict the types of inference explosion that can otherwise arise with such rules. The genealogy theory itself draws on the simple personal relationship information contained in the employment theory 20. This is a further type of theory-to-theory relationship, between two object theories.

Returning to the employment theory 20, its assimilator theory 24 also takes account of a further type of constraint pertaining to the "meaning" of the data, for instance whether a new employee's relationship that is being added is consistent with the theory and with the knowledge about relationships held in the genealogy theory. This will involve the assimilator requiring results to be proved in the genealogy theory.

The present invention is concerned with an architecture for organising theories in a theory-based system. The prior art only addresses the issue of theory reference in terms of references to one theory within another. The issue of the overall organisation of theories in a theory-based system is not addressed at all.

According to the present invention there is provided, in a system comprising a plurality of object theories and metatheories having coupling relationships between them, an inference engine, and query processing means, the method of processing queries comprising: providing a system theory which defines the coupling relationships between the theories, processing the query by the system theory to choose an object theory and associated metatheories in dependence on the parameters of the query and processing of the query by the theories so chosen. The present invention thus provides a new system arhitecture for a theory-based system and one which gives rise to substantial technical advantages as will be explained.

BRIEF DESCRIPTION OF THE DRAWINGS

FIG. 1 depicts known types of partitioning.

FIG. 2 shows the main components of a system according to the present invention.

FIG. 3 depicts the updating of a theory having a name TN according to the teachings of the invention.

DETAILED DESCRIPTION OF THE INVENTION

A system theory provides an organisation of the theories it contains. Since it is itself a theory it can participate in higher level organisations of system theories. This higher level organisation therefore contains many system theories which may be an evolution of one system theory or an organisation of several evolutions of unconnected system theories. This higher level organisation could itself be described by a theory and so could participate in even higher level organisations and so on.

A system theory can be regarded as an architecture which supports the storage, retrieval and updating of knowledge modularised into separate theories. Each theory in the system is associated with three other theories. All three are metatheories with respect to that theory, which correspondingly is an object theory with respect to those metatheories. First, there is an interpreter metatheory, which defines a provability relationship for the object theory, supporting query satisfaction as theorem proving. The interpreter controls inference within the object theory, supporting explicit, domain-specific characterizations of the object theory clauses where available. Second, there is an assimilator metatheory, which extends the logical update primitives provided by the underlying knowledge base management system to enforce syntactic and semantic constraints (both local and global) on updates of the object theory. Third, there is an attribute metatheory which expresses characteristics of the object theory clauses, such as type constraints, used by interpreters and assimilators to control inference and updating.

The partitioning of this theory-specific metaknowledge allows interpreters and assimilators to be shared amongst several different object theories.

An interpreter theory may for example incorporate means for backtracking through a succession of theories having an inheritance relationship. One form of inheritance is merely theory selection, where a goal is proved in one member of a set of theories with an inheritance relationship. A more elaborate form of inheritance can readily be incorporated in a theory's interpreter, such that when the interpreter tries to satisfy a goal in a named theory and fails, it does not back-track to the previous goal; instead, it queries the system to find the name of a theory from which the current theory inherits and tries to satisfy the current goal in the ancestral theory. This elaboration allows each individual subgoal to be tried in each theory, instead of only the overall goal.

The primary use of attribute theories is to allow particular theory-dependent information to be abstracted out of interpreters and assimilators. This enables the interpreters and assimilators to be made relatively independent of particular theories and hence to be applicable to more than one object theory.

All assimilation proceeds via a standard interface, like the standard query interface, update(System,TheoryName,Updates,NewSystem,NewTheory). In a similar manner to interpretation, each assimilator must understand and be able to translate into, the representation of the theory it is updating. An update is specified as a list of actions--all actions are eventually reduced to primitive declarative add and delete operations on the theory being updated. The simplest form of assimilator simply carries out such additions and deletions. A more elaborate assimilator will carry out some form of checking for consistency either clause by clause as they are added (with provision for ignoring unavoidably inconsistent states of the theory during updating) or on the theory as fully updated; in either case, there is provision for backtracking and restoration of the original state of the theory in the event of an attempted illegal update. As with interpreter theories, the abstraction of consistency checking from a theory into an assimilator theory makes it more likely that an assimilator theory will be applicable to more than one theory. The system theory itself also has its own assimilator. A typical task for the system assimilator might be to check that when a new theory is being added to the system, all of its nominated metatheories also belong to the system.

Since interpreters and assimilators are themselves theories, they also may be associated with metatheories. An interpreter theory (object theory) will in turn require another interpreter theory (metatheory) to control inference within the first interpreter theory. Likewise assimilator theories and attribute theories will require interpreter theories. Conversely, interpreter and assimilator theories may also require attribute theories and so on. However, only one or two levels of interpretation will be used in practice, for reasons of efficiency. This apparent infinite regress is terminated by special built-in interpreter and assimilation theories.

In the architecture of the invention a knowledge base is represented by a special type of theory, the system theory, but one which is distinguished only by its role. The system theory is a declarative statement of all theories in the system and the relationships between them. The system theory describes the relationship between the name of a theory, the theory itself and the names of its metatheories. In defining this relationship, the full power of Horn clause logic can be brought to bear. For example, a named object theory can have many interpreters and a particular interpreter may be used on many object theories. The system ability to represent many-to-many relationships between theories and their metatheories and allows reasoning within the system about which metatheory is appropriate for a particular task.

In the preferred arrangement, the system theory statement are preferably five-place clauses, with one place for a theory name and the other four places corresponding respectively to an object theory, an interpreter metatheory, an assimilator metatheory and an attribute metatheory therefor.

    ______________________________________
    An example of the
    form of statements in the system theory is shown below:
    Theory
    Name        Theory  Interpreter
                                  Assimilator
                                          Attribute
    ______________________________________
    "theory"
           (calc,   T.sub.1,
                            prologInt,
                                    prologAss,
                                            none)
    "theory"
           (calc,   T.sub.1,
                            calcInt prologAss,
                                            none)
    "theory"
           (calcInt,
                    T.sub.2,
                            prologInt,
                                    prologAss,
                                            none)
    "theory"
           (calcInt,
                    T.sub.2,
                            prologInt,
                                    calcAss,
                                            none)
    "theory"
           (calcAss,
                    T.sub.3,
                            prologInt,
                                    prologAss,
                                            none)
    "theory"
           (system, T.sub.4,
                            prologInt,
                                    prolog Ass,
                                            none)
    ______________________________________

    ______________________________________
    prove (System, system, Goals):- interpretTheory
                              (Clause 1)
    (System, Goals).
    prove (System, prologInt, interpret (TheoryName,
                              (Clause 2)
    Theory AttrName, Goals):-
    interpretTheory (Theory, Goals).
    prove(System, TheoryName, Goals):-
                              (Clause 3)
    prove(System, system, theory(TheoryName, Theory, IntName,
    AssName, AttrName).
    prove(System, Intname, interpret(TheoryName, Theory,
    AttrName, Goals).
    update(System, TheoryName, Clauses, NewSystem, NewTheory):-
    prove(System, system, theory(TheoryName, Theory, IntName,
    AssName, AttrName))
    prove(System, AssName, assimilate(System, Theory, AttrName,
    Clauses, NewTheory), updateSystem
    (System, TheoryName, Theory, New Theory, NewSystem).
    ______________________________________

    ______________________________________
    The system theory comprises the following statements:
    ______________________________________
    theory (system, Theory,
                      <- system(Theory) & true
    prologint, prologAss, none)
    theory (fib, theory-a80f8,
                      <- true
    prologint, prologAss, none)
    theory (lemma, theory-a8510,
                      <- true
    prologint, prologAss, none)
    theory (fibbattr, theory-a8638,
                      <- true
    prologint, prologAss, none)
    theory (fibl, theory-a8734,
                      <- true
    lemma, prologAss, fibattr)
    theory (myprove, theory-a8bd8,
                      <- true
    prologint, prologAss, none)
    theory (myprove, theory-a8bd8,
    prologint, prologAss, none)
                      <- true
    ______________________________________
    Reference numbers for the relevant theories appear in the second
    places in each statement for the purpose of this description, in
    actuality the whole Theory term resides in those positions.
    ______________________________________
    The query is:
    prove (System, fib, fib(8, N))
    ______________________________________
    The steps in the prove process are shown below:
    ______________________________________
    clause 3 (call): prove(theory-a8f84, fib, fib(8, N))
                                   C1
    clause 1 (call): prove(theory-a8f84, system, theory(fib,
                                   C2
    Theory, IntName, AssName, AttrName))
    clause 1 (call): interpretTheory(theory-a8f84, theory(fib,
                                   C3
    Theory, IntName, AssName, AttrName))
    clause 1 (exit): interpretTheory(theory-a8f84, theory(fib,
                                   E3
    theory-a80f8, prologint, prologAss, none))
    clause 1 (exit): prove(theory-a8f84, system, theory(fib,
                                   E2
    theory-a80f8, prologint, prologAss, none))
    clause 2 (call): prove(theory-a8f84, prologint, interpret(fib,
                                   C4
    theory-a80f8, none, fib(8, N))
    clause 1 (call): interpretTheory(theory-a80f8, fib(8, N))
                                   C5
    clause 1 (exit): interpretTheory(theory-a80f8, fib(8, 34))
                                   E5
    clause 2 (exit): prove(theory-a8f84, prologint, interpret(fib,
                                   E4
    theory-a80f8, none, fib(8, 34))
    clause 3 (exit): prove(theory-a8f84, fib, fib(8, 34))
                                   E1
    ______________________________________

    ______________________________________
    The system theory comprises the following statements:
    ______________________________________
    theory(system, Theory, prologInt,
                        <- system(Theory) & true
    prologAss, none)
    theory(fib, theory-aa12c, prologInt,
                        <- true
    prologAss, none)
    theory(lemma, theory-a86bc,
                        <- true
    prologInt, prologAss, none)
    theory(fibattr, theory-a87e4,
                        <- true
    prologInt, prologAss, none)
    theory(fibl, theory-a88e0, lemma,
                        <- true
    prologAss, fibattr)
    theory(myprove, theory-a8d84,
                        <- true
    prologInt, prologAss, none)
    theory(prologAss, theory-a94d8,
                        <- true
    prologInt, prologAss, none)
    nil
    ______________________________________
    The steps in the "update" process are shown below:
    ______________________________________
    clause 1 (call): myupdate(theory-a96ac, fib, assert(fib(-1,
                                   C1),
    nil, S7, NT)
    clause 1 (call): prove(theory-a96ac, system, theory(fib,
                                   C2eory,
    IntName, AssName, AttrName))
    clause 1 (call): interprettheory(theory-a96ac, theory(fib,
                                   C3
    Theory, IntName, AssName, AttrName))
    clause 1 (exit): interpretTheory(theory-a96ac, theory(fib,
                                   E3
    theory-a82a4, prologInt, prologAss, none))
    clause 1 (exit): prove(theory-a96ac, system, theory(fib,
                                   E2
    theory-a82a4, prologInt, prologAss, none))
    clause 3 (call): prove(theory-a96ac, prologAss, assimilate
                                   C4
    (theory-a96ac, theory-a82a4, none, assert(fib(-1, 0)),
    nil, NT))
    clause 1 (call): prove(theory-a96ac, system, theory(prologAss,
                                   C5
    Theory, IntName,, AssName, AttrName))
    clause 1 (call): interpretTheory(theory-a96ac,
                                   C6
    theory(prologAss, Theory, IntName, AssName, AttrName))
    clause 1 (exit): interpretTheory(theory-a96ac,
                                   E6
    theory(prologAss, theory-a94d8, prologInt, prologAss, none))
    clause 1 (exit): prove(theory-a96ac, system, theory(prologAss,
                                   E5
    theory-a94d8, prologInt, prologAss, none)
    clause 2 (call): prove(theory-a96ac, prologInt,
                                   C7
    interpret(prologAss, theory-a94d8, none,
    assimilate(theory-a96ac, theory-a82a4, none,
    assert(fib(-1, 0)), nil, NT))
    clause 1 (exit): interpretTheory(theory-a94d8,
                                   E8
    assimilate(theory-a96ac, theory-a82a4, none,
    assert(fib(-1,0)), nil, theory-aa12c))
    clause 2 (exit): prove(theory-a96ac, prologInt,
                                   E7
    interpret(prologAss, theory-a94d8, none, assimilate
    (theory-a96ac, theory-a82a4, none, assert(fib-1, 0)), nil,
    theory-aa12c))
    clause 3 (exit): prove(theory-a96ac, prologAss,
                                   E4
    assimilate(theory-a96ac, theory-a82a4, none,
    assert(fib(-1, 0)), nil, theory-aa12c))
    clause 1 (call): updateSystem(theory-a96ac, fib, theory-a82a4,
                                   C9
    theory-aa12c, S7)
    clause 1 (exit): updateSystem(theory-a96ac, fib, theory-a82a4,
                                   E9
    theory-aa12c, theory-aa1f4)
    clause 1 (exit): myupdate(theory-a96ac, fib, assert(fib(-1,
                                   E1),
    nil, theory-aa1f4, theory-aa12c)
    ______________________________________

                                      APPENDIX A
    __________________________________________________________________________
    fib.pl loading . . .
    fib.pl loaded.
    lemma.pl loading . . .
    lemma. pl loaded.
    fibattr loading . . .
    fibattr loaded.
    fib.pl loading . . .
    fib.pl loaded.
    myprove loading. . .
    myprove loaded.
    prologAss.pl loading . . .
    prologAss.pl loaded.
    The System Theory
    theory(system, Theory, prologInt, prologAss, none) <-
    system(theory) & true.
    theory(fib, #fib(0, 1) <- true.
    fib(1, 1) <- true.
    fib(N, M3) <-
    N > 1 &
    M is N - 1 &
    M1 is N - 2 &
    fib(M, FM) &
    fib(M1, FM1) &
    M3 is FM + FM1 & true.
    nil
    , prologInt, prologAss, none) <- true.
    theory(lemma, #interpret(TheoryName, Theory, AttrName, Goals) <-
    call(Theory, Goals) & true.
    nil
    , prologInt, prologAss, none) <- true.
    theory(fibattr, #uniqueSoln(fib(X, .sub.-)) <-
    ground(X) &
    ! & true.
    nil
    , prologInt, prologAss, none) <- true.
    theory(fibl, #fib(0, 1) <- true.
    fib(1, 1) <- true.
    fib(N, M3) <-
    N > 1 &
    M is N - 1 &
    M1 is N - 2 &
    fib(M, FM) &
    fib(M1, FM1) &
    M3 is FM + FM1 & true.
    nil
    , lemma, prologAss, fibatttr) <- true.
    theory(myprove, #myupdate(System, TheoryName, Clauses, NewSystem,
    NewTheory) <-
    write('clause 1 (call): ') &
    write(update(System, TheoryName, Clauses, NewSystem, NewTheory)) &
    nl &
    myprove(System, system, theory(TheoryName, Theory, IntName, AssName,
    AttrName)) &
    myprove(System, AssName, assimilate(System, Theory, AttrName, Clauses,
    NewTheory)) &
    updatesSystem(System, TheoryName, Theory, NewTheory, NewSystem) &
    write('clause 1 (exit): ') &
    write(update(System, TheoryName, Clauses, NewSystem, NewTheory)) &
    nl & true.
    updateSystem(System, TheoryName, Theory, NewTheory, NewSystem) <-
    write('clause 1 (call): ') &
    write(updateSystem(System, TheoryName, Theory, NewTheory, NewSystem)) &
    nl &
    update(system, replace(theory(TheoryName, Theory, IntName, AssName,
    AttrName) <- true,
    theory(TheoryName, NewTheory, IntName, AssName, AttrName) <- true) . nil,
    System, NewSystem
    write('clause 1 (exit): ') &
    write(updateSystem(System, TheoryName, Theory, NewTheory, NewSystem)) &
    nl & true.
    interpretTheory(T, G) <-
    write('clause 1 (call): ') &
    write(interpretTheory(T, G)) &
    nl &
    call(T, G) &
    write('clause 1(exit): ') &
    write(interpretTheory(T, G)) &
    nl & true.
    myprove(System, system, Goals) <-
    write('clause 1 (call): ' ) &
    write(prove(System, system, Goals)) &
    nl &
    interpretTheory(System, Goals) &
    write('clause 1 (exit): ') &
    write(prove(System, system, Goals)) &
    nl & true.
    myprove(System, prologint, interpret(TheoryName, Theory, AttrName,
    Goals)) <-
    write('clause 2 (call): ') &
    write(prove(System, prologInt, interpret(TheoryName, Theory, AttrName,
    Goals))) &
    nl &
    interpretTheory(Theory, Goals) &
    write('clause 2 (exit): ') &
    write(prove(System, prologInt, interpret(TheoryName, Theory, AttrName,
    Goals))) &
    nl & true.
    myprove(System, TheoryName, Golas) <-
    write('clause 3 (call): ') &
    write(prove(System, TheoryName, Goals)) &
    nl &
    myprove(System, system, theory(TheoryName, Theory, IntName, AssName,
    AttrName)) &
    myprove(System, IntName, interpret(TheoryName, Theory, AttrName, Goals))
    write('clause 3 (exit): ') &
    write(prove(System, TheoryName, Goals)) &
    nl & true.
    nil
    , prologInt, prologAss, none) <- true.
    theory(prologAss, #assimilate(.sub.-, T, .sub.-, nil, T) <- true.
    assimilate(S, T, .sub.-, assert(C) . Rest, NT) <-
    normalize(C, NC) &
    assertz(T, T1, NC) &
    assimilate(S, T1, .sub.-, Rest, NT) & true.
    assimilate(S, T, .sub.-, retract(C) . Rest, NT) <-
    normalize(C, NC) &
    retract(T, T1, NC) &
    assimilate(S, T1, .sub.-, Rest, NT) & true.
    nil
    prologInt, prologAss, none) <- true.
    SUCCESS
    INTERPRET TIME: 640 ms
    INFERENCE STEPS: 243
    __________________________________________________________________________

• Inventors
  Black, Damian S.; Manley, John C.;
• Assignee
  Hewlett-Packard Company (Palo Alto, CA)
• Published
  Jul-6-1993
• Current US Classes:
  706/46
  706/50
  707/104.1
• Application #
  682754
• International Classes
  G06F 015/18; G06F 015/40
• Field of Search
  395/54 395/51 395/52 395/53 395/66 395/67 395/62 395/903 395/904 395/600 364/DIG.
• Examiner
  Ruggiero; Joseph
• US Patent References:
  4884218
  4888690
  4930071
  5016204
  5025392
  5063522
  5065338