Disjunctive unification

Claim 3

The system of claim 1 in which the first term of the logical formula includes a first value and the second term of the logical formula includes a second value, the first data unit including a first value token indicating the first value and the second data unit including a second value token indicating the second value.

Claim 4

The system of claim 2 in which each of the first and second terms of the logical formula includes a feature that can take either of the first and second values; the processor further comprising third means for producing a third data unit as a result of unifying the first and second data units, the third data unit including a feature token indicating the feature.

Claim 5

The system of claim 1 in which the first context is one of a first set of genuine alternatives and the second context is one of a second set of genuine alternatives, the second means determining to unify the first and second data units based on the first and second context identifiers.

Claim 6

The system of claim 1 in which the first context identifier includes a first number identifying a set of genuine alternatives that includes the first context and a second number identifying the first context.

Claim 7

The system of claim 1 in which the first term is a disjunct that includes a value, the first data unit including the first context identifier and a value token indicating the value.

Claim 8

The system of claim 6 in which the disjunct further includes a feature that can take the value, the first data unit including a feature token indicating the feature.

Claim 9

The system of claim 1 in which the first data unit includes the first context identifier.

Claim 10

The system of claim 1 in which the first context is a null context that includes the respective contexts of all of the disjuncts of the logical formula.

Claim 11

The system of claim 1 in which the processor further comprises third means for unifying the first and second data units to produce a unified data unit if the second means determines to unify the first and second data units.

Claim 12

The system of claim 10 in which the third means is further for unifying the first and second context identifiers to produce a unified context identifier indicating a third context that includes the intersection of the first and second contexts, the third means unifying the first and second context identifiers if the second means determines to unify the first and second data units.

Claim 13

The system of claim 10 in which the processor further comprises fourth means for using the unified data unit to obtain a solution of the logical formula.

Claim 14

The system of claim 1 in which the processor further comprises third means for producing the first and second data units and the first and second context identifiers from the logical formula.

Claim 15

The system of claim 13 in which the third means produces the first data unit so that the first data unit includes the first context identifier.

Claim 18

The method of claim 15 in which the second context is different than the first context, the step of using the first and second context identifiers further comprising a substep of determining whether the first and second contexts are genuine alternatives based on the first and second context identifiers.

Claim 19

The method of claim 16 in which the first and second contexts are members of a set of genuine alternatives, the first context identifier including a first number identifying the set of genuine alternatives and a second number identifying the first context, the second context identifier including the first number and a third number identifying the second context; the substep of determining whether the first and second contexts are genuine alternatives comprising a substep of determining that they are genuine alternatives based on the first, second, and third numbers.

Claim 20

The method of claim 16 further comprising, if the first and second contexts are not genuine alternatives, a step of unifying the first and second data units to obtain a unified data unit; the step of using the first and second context identifiers determining not to unify the first and second data units if the first and second contexts are genuine alternatives.

Claim 21

The method of claim 18 in which each of the first and second data units includes a respective value token corresponding to a respective value; the step of unifying the first and second data units comprising a substep of determining whether the first and second data units are consistent based on whether their respective value tokens are consistent.

Claim 22

The method of claim 15 in which each of the first and second data units includes a respective value token corresponding to a respective value; the method further comprising, if the step of using the first and second context identifiers determines to unify the first and second data units, a step of unifying the first and second data units; the step of unifying the first and second data units comprising a substep of determining whether the first and second data units are consistent based on whether their respective value tokens are consistent.

Claim 23

The method of claim 15 in which the first and second data units include first and second value data units, respectively, the first and second value data units including first and second feature-value pairs, respectively; the second feature-value pair including a feature token and a value token; the method further comprising, if the step of using the first and second context identifiers determines to unify the first and second data units, a step of unifying the first and second data units; the step of unifying the first and second data units comprising unifying the value token with an indeterminate disjunctive value data unit to obtain a unified disjunctive value data unit and then including [the]a third feature-value pair including the feature token and the unified disjunctive value data unit in the first value data unit.

Claim 24

The method of claim 15 in which the method further comprises, if the step of using the first and second context identifiers determines to unify the first and second data units, a step of unifying the first and second data units; the unifying step comprising a substep of performing propositional reasoning with the first and second context identifiers.

Claim 25

The method of claim 15 in which the system further includes a third context identifier that indicates a third context in which to unify the first and second data units; the step of using the first and second context identifiers further comprising a substep of using the third context identifier in determining whether to unify the first and second data units.

Claim 26

The method of claim 23 in which the substep of using the third context identifier comprises a substep of determining whether the third context intersects with each of the first and second contexts based on the first, second, and third context identifiers.

Claim 27

The method of claim 23 in which the first data unit includes the first context identifier, the method further comprising, if the step of using the first and second context identifiers determines to unify the first and second data units, a step of unifying the first and second data units; the unifying step comprising a substep of positioning a pointer to the first data unit in the second data unit.

Claim 28

The method of claim 15 in which the method further comprises, if the step of using the first and second context identifiers determines to unify the first and second data units, a step of unifying the first and second data units; the unifying step comprising a substep of unifying the first and second data units to obtain a unified data unit.

Claim 29

The method of claim 15 in which the method further comprises, if the step of using the first and second context identifiers determines to unify the first and second data units, a step of unifying the first and second data units.

Claim 30

The method of claim 27 in which the method further comprises, if the step of using the first and second context identifiers determines to unify the first and second data units, a step of merging the first and second context identifiers, the unifying step producing a unified data unit and the merging step producing a merged context identifier identifying a merged context.

Claim 31

The method of claim 28 in which the first data unit includes a first feature token and a first value token, the unifying step comprising a substep of producing the unified data unit so that it includes the first feature token and a subunit, the subunit including the first context identifier and the first value token.

Claim 32

The method of claim 29 in which the second data unit includes a second feature token equal to the first feature token and a second value token different than the first value token, the unifying step further comprising a substep of producing the unified data unit so that the subunit includes the second context identifier and the second value token.

Claim 33

The method of claim 30 in which the merged context is a null context that includes the respective contexts of all of the disjuncts of the logical formula, the method further comprising a step of eliminating the merged context identifier.

Claim 34

The method of claim 27 in which the method further comprises, if the step of using the first and second context identifiers determines to unify the first and second data units, a step of using the first and second context identifiers to produce a third context identifier.

Claim 35

The method of claim 32 in which the first context identifier indicates that the first context is a null context that includes the respective contexts of all the disjuncts of the logical formula, the step of using the first and second context identifiers comprising choosing the second context identifier as the third context identifier.

Claim 36

The method of claim 32 in which the first and second context identifiers indicate that the first and second contexts are equal, the step of using the first and second context identifiers comprising choosing the first context identifier as the third context identifier.

Claim 37

The method of claim 32 in which the step of using the first and second context identifiers comprises a substep of finding an intersection of the first and second contexts, the third context identifier identifying the intersection of the first and second contexts.

Claim 38

The method of claim 27 in which the first and second data units include first and second feature-value pairs, respectively; the first feature-value pair including a first feature token indicating a first feature and a first value data unit indicating a first value; the second feature-value pair including a second feature token indicating a second feature and a second value data unit indicating a second value; the first feature and the second feature being different features; the step of unifying the first and second data units comprising a substep of adding the second feature value pair to the first data unit.

Claim 39

The method of claim 27 in which the first and second data units include first and second feature-value pairs, respectively; the first feature-value pair including a first feature token indicating a first feature and a first value data unit indicating a first value; the second feature-value pair including a second feature token indicating the first feature and a second value data unit indicating a second value; the step of unifying the first and second data units comprising a substep of unifying the first and second value data units.

Claim 40

The method of claim 27 in which the step of unifying the first and second data units produces a unified data unit, the method further comprising a step of using the unified data unit to obtain a solution of the logical formula.

Claim 41

The method of claim 15 in which the first context is a null context that includes the respective contexts of all the disjuncts of the logical formula.

Claim 42

The method of claim 15, further comprising a step of producing the first and second data units and the first and second context identifiers from the logical formula.

Claim 43

The method of claim 40 in which the step of producing the first and second data units and the first and second context identifiers comprises a substep of producing the first data unit so that the first data unit includes the first context identifier.

Claim 44

A computer system for solving a logical formula using unification, the logical formula including a plurality of terms; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the system comprising: memory; a first data unit and a second data unit stored in the memory, the first data unit including data relating to a first one of the terms of the logical formula and the second data unit including data relating to a second one of the terms of the logical formula; a first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; a second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the first and second context identifiers being stored in the memory; and a processor for performing unification, the processor being connected for accessing the memory; the processor including: first means for accessing the first data unit and the second data unit and the first and second context identifiers in the memory; and second means for using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 45

A computer system for solving a logical formula using unification, the logical formula including a plurality of terms; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the system comprising: memory; a first data unit and a second data unit stored in the memory, the first data unit including data relating to a first one of the terms of the logical formula and the second data unit including data relating to a second one of the terms of the logical formula; a first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; a second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the first and second context identifiers being stored in the memory; and a processor for performing unification, the processor being connected for accessing the memory; the processor including: first means for accessing the first data unit and the second data unit and the first and second context identifiers in the memory; and second means for using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 46

A computer-implemented method of solving a logical formula using unification, the logical formula including a plurality of terms; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the method being performed with a computer system that includes: memory; a first data unit and a second data unit stored in the memory, the first data unit including data relating to a first one of the terms of the logical formula and the second data unit including data relating to a second one of the terms of the logical formula; a first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; a second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the first and second context identifiers being stored in the memory; and a processor connected for accessing the first and second data units and the first and second context identifiers in the memory and for performing unification; the method comprising steps of: accessing the first data unit and the second data unit and the first and second context identifiers in the memory; and using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 47

A computer-implemented method of solving a logical formula using unification, the logical formula including a plurality of terms; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the method being performed with a computer system that includes: memory; a first data unit and a second data unit stored in the memory, the first data unit including data relating to a first one of the terms of the logical formula and the second data unit including data relating to a second one of the terms of the logical formula; a first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; a second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the first and second context identifiers being stored in the memory; and a processor connected for accessing the first and second data units and the first and second context identifiers in the memory and for performing unification; the method comprising steps of: accessing the first data unit and the second data unit and the first and second context identifiers in the memory; and using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 48

A computer system for solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the system comprising: memory; a first data unit and a second data unit stored in the memory, the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; a first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; a second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the first and second context identifiers being stored in the memory; and a processor for performing unification, the processor being connected for accessing the memory; the processor including: first means for accessing the first data unit and the second data unit and the first and second context identifiers in the memory; and second means for using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 49

A computer system for solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the system comprising: memory; a first data unit and a second data unit stored in the memory, the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; a first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; a second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the first and second context identifiers being stored in the memory; and a processor for performing unification, the processor being connected for accessing the memory; the processor including: first means for accessing the first data unit and the second data unit and the first and second context identifiers in the memory; and second means for using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 50

A computer-implemented method of solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the method being performed with a computer system that includes: memory; a first data unit and a second data unit stored in the memory, the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; a first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; a second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the first and second context identifiers being stored in the memory; and a processor connected for accessing the first and second data units and the first and second context identifiers in the memory and for performing unification; the method comprising steps of: accessing the first data unit and the second data unit and the first and second context identifiers in the memory; and using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 51

A computer-implemented method of solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the method being performed with a computer system that includes: memory; a first data unit and a second data unit stored in the memory, the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; a first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; a second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the first and second context identifiers being stored in the memory; and a processor connected for accessing the first and second data units and the first and second context identifiers in the memory and for performing unification; the method comprising steps of: accessing the first data unit and the second data unit and the first and second context identifiers in the memory; and using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 52

A computer system for solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the system comprising: memory; a first data unit and a second data unit stored in the memory, the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; a first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; a second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the first and second context identifiers being stored in the memory; unification instruction data stored in the memory; the unification instruction data indicating first unification instructions and second unification instructions; and a processor connected for accessing the memory; the processor accessing the unification instruction data and executing the first unification instructions and the second unification instructions to perform unification of the first and second data units; the processor, in executing the first unification instructions, accessing the first data unit and the second data unit and the first and second context identifiers in the memory; the processor, in executing the second unification instructions, using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 53

A computer system for solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the system comprising: memory; a first data unit and a second data unit stored in the memory, the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; a first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; a second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the first and second context identifiers being stored in the memory; unification instruction data stored in the memory; the unification instruction data indicating first unification instructions and second unification instructions; and a processor connected for accessing the memory; the processor accessing the unification instruction data and executing the first unification instructions and the second unification instructions to perform unification of the first and second data units; the processor, in executing the first unification instructions, accessing the first data unit and the second data unit and the first and second context identifiers in the memory; the processor, in executing the second unification instructions, using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 54

A computer-implemented method of solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the method being performed with a computer system that includes: memory; a first data unit and a second data unit stored in the memory, the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; a first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; a second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the first and second context identifiers being stored in the memory; unification instruction data stored in the memory; the unification instruction data indicating first unification instructions and second unification instructions; and a processor connected for accessing the memory; the processor executing the first unification instructions and the second unification instructions to perform unification of the first and second data units; the method comprising: operating the processor to access the unification instruction data and execute the first unification instructions; the processor, in executing the first unification instructions, accessing the first data unit and the second data unit and the first and second context identifiers in the memory; and operating the processor to access the unification instruction data and execute the second unification instructions; the processor, in executing the second unification instructions, using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 55

A computer-implemented method of solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the method being performed with a computer system that includes: memory; a first data unit and a second data unit stored in the memory, the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; a first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; a second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the first and second context identifiers being stored in the memory; unification instruction data stored in the memory; the unification instruction data indicating first unification instructions and second unification instructions; and a processor connected for accessing the memory; the processor executing the first unification instructions and the second unification instructions to perform unification of the first and second data units; the method comprising: operating the processor to access the unification instruction data and execute the first unification instructions; the processor, in executing the first unification instructions, accessing the first data unit and the second data unit and the first and second context identifiers in the memory; and operating the processor to access the unification instruction data and execute the second unification instructions; the processor, in executing the second unification instructions, using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 56

A computer system for solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the system comprising: memory; formula data stored in memory; the formula data defining the logical formula; unification instruction data stored in the memory; the unification instruction data indicating first unification instructions and second unification instructions; and a processor connected for accessing the memory; the processor accessing the formula data and the unification instruction data and executing the first unification instructions and the second unification instructions to perform unification; the processor, in executing the first unification instructions, accessing the formula data in the memory and using the formula data to produce first and second data units and first and second context identifiers and storing the first and second data units and the first and second context identifiers in the memory; the first data unit including the first context identifier and the second data unit including the second context identifier; the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; the first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; the second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the processor, in executing the second unification instructions, accessing the first data unit and the second data unit and the first and second context identifiers in the memory and using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 57

A computer system for solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the system comprising: memory; formula data stored in memory; the formula data defining the logical formula; unification instruction data stored in the memory; the unification instruction data indicating first unification instructions and second unification instructions; and a processor connected for accessing the memory; the processor accessing the formula data and the unification instruction data and executing the first unification instructions and the second unification instructions to perform unification; the processor, in executing the first unification instructions, accessing the formula data in the memory and using the formula data to produce first and second data units and first and second context identifiers and storing the first and second data units and the first and second context identifiers in the memory; the first data unit including the first context identifier and the second data unit including the second context identifier; the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; the first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; the second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; the processor, in executing the second unification instructions, accessing the first data unit and the second data unit and the first and second context identifiers in the memory and using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 58

A computer-implemented method of solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the method being performed with a computer system that includes: memory; formula data stored in memory; the formula data defining the logical formula; unification instruction data stored in the memory; the unification instruction data indicating first unification instructions and second unification instructions; and a processor connected for accessing the memory; the processor accessing the formula data and the unification instruction data and executing the first unification instructions and the second unification instructions to perform unification; the method comprising: operating the processor to access the unification instruction data and execute the first unification instructions; the processor, in executing the first unification instructions, accessing the formula data in the memory and using the formula data to produce first and second data units and first and second context identifiers and storing the first and second data units and the first and second context identifiers in the memory; the first data unit including the first context identifier and the second data unit including the second context identifier; the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; the first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; the second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; operating the processor to access the unification instruction data and execute the second unification instructions; the processor, in executing the second unification instructions, accessing the first data unit and the second data unit and the first and second context identifiers in the memory and using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 59

A computer-implemented method of solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the method being performed with a computer system that includes: memory; formula data stored in memory; the formula data defining the logical formula; unification instruction data stored in the memory; the unification instruction data indicating first unification instructions and second unification instructions; and a processor connected for accessing the memory; the processor accessing the formula data and the unification instruction data and executing the first unification instructions and the second unification instructions to perform unification; the method comprising: operating the processor to access the unification instruction data and execute the first unification instructions; the processor, in executing the first unification instructions, accessing the formula data in the memory and using the formula data to produce first and second data units and first and second context identifiers and storing the first and second data units and the first and second context identifiers in the memory; the first data unit including the first context identifier and the second data unit including the second context identifier; the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; the first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; the second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; operating the processor to access the unification instruction data and execute the second unification instructions; the processor, in executing the second unification instructions, accessing the first data unit and the second data unit and the first and second context identifiers in the memory and using the first and second context identifiers to determine whether to unify the first and second data units.

Claim 60

A computer system for solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the system comprising: memory; formula data stored in memory; the formula data defining the logical formula; unification instruction data stored in the memory; the unification instruction data indicating first unification instructions, second unification instructions, third unification instructions, and fourth unification instructions; and a processor connected for accessing the memory; the processor accessing the formula data and the unification instruction data and executing the first unification instructions, the second unification instructions, the third unification instructions, and the fourth unification instructions to solve the logical formula; the processor, in executing the first unification instructions, accessing the formula data in the memory and using the formula data to produce first and second data units and first and second context identifiers and storing the first and second data units and the first and second context identifiers in the memory; the first data unit including the first context identifier and the second data unit including the second context identifier; the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; the first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; the second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula, the first context applying to the first data unit and the second context applying to the second data unit; the processor, in executing the second unification instructions, accessing the first data unit and the second data unit and the first and second context identifiers in the memory and using the first and second context identifiers to determine whether to execute the third unification instructions and the fourth unification instructions; the processor, in executing the third unification instructions, unifying the first and second data units to obtain a unified data unit and storing the unified data unit in the memory; the processor, in executing the fourth unification instructions, accessing the unified data unit in the memory and using the unified data unit to obtain solution data indicating a solution of the logical formula, the solution data including linguistic information about the logical formula.

Claim 61

A computer system for solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the system comprising: memory; formula data stored in memory; the formula data defining the logical formula; unification instruction data stored in the memory; the unification instruction data indicating first unification instructions, second unification instructions, third unification instructions, and fourth unification instructions; and a processor connected for accessing the memory; the processor accessing the formula data and the unification instruction data and executing the first unification instructions, the second unification instructions, the third unification instructions, and the fourth unification instructions to solve the logical formula; the processor, in executing the first unification instructions, accessing the formula data in the memory and using the formula data to produce first and second data units and first and second context identifiers and storing the first and second data units and the first and second context identifiers in the memory; the first data unit including the first context identifier and the second data unit including the second context identifier; the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; the first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; the second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula, the first context applying to the first data unit and the second context applying to the second data unit; the processor, in executing the second unification instructions, accessing the first data unit and the second data unit and the first and second context identifiers in the memory and using the first and second context identifiers to determine whether to execute the third unification instructions and the fourth unification instructions; the processor, in executing the third unification instructions, unifying the first and second data units to obtain a unified data unit and storing the unified data unit in the memory; the processor, in executing the fourth unification instructions, accessing the unified data unit in the memory and using the unified data unit to obtain solution data indicating a solution of the logical formula, the solution data including linguistic information about the logical formula.

Claim 62

A computer-implemented method of solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the method being performed with a computer system that includes: memory; formula data stored in memory; the formula data defining the logical formula; unification instruction data stored in the memory; the unification instruction data indicating first unification instructions, second unification instructions, third unification instructions, and fourth unification instructions; and a processor connected for accessing the memory; the processor accessing the formula data and the unification instruction data and executing the first unification instructions, the second unification instructions, the third unification instructions, and the fourth unification instructions to solve the logical formula; the method comprising: operating the processor to access the unification instruction data and execute the first unification instructions; the processor, in executing the first unification instructions, accessing the formula data in the memory and using the formula data to produce first and second data units and first and second context identifiers and storing the first and second data units and the first and second context identifiers in the memory; the first data unit including the first context identifier and the second data unit including the second context identifier; the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; the first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; the second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; operating the processor to access the unification instruction data and execute the second unification instructions; the processor, in executing the second unification instructions, accessing the first data unit and the second data unit and the first and second context identifiers in the memory and using the first and second context identifiers to determine whether to execute the third unification instructions and the fourth unification instructions; operating the processor to access the unification instruction data and execute the third unification instructions; the processor, in executing the third unification instructions, unifying the first and second data units to obtain a unified data unit and storing the unified data unit in the memory; operating the processor to access the unification instruction data and execute the fourth unification instructions; the processor, in executing the fourth unification instructions, accessing the unified data unit in the memory and using the unified data unit to obtain solution data indicating a solution of the logical formula, the solution data including linguistic information about the logical formula.

Claim 63

A computer-implemented method of solving a logical formula that contains linguistic information using unification, the logical formula including a plurality of terms that contain linguistic information; at least one of the terms including a disjunction, each disjunction having a plurality of disjuncts, each disjunct having a respective context; the method being performed with a computer system that includes: memory; formula data stored in memory; the formula data defining the logical formula; unification instruction data stored in the memory; the unification instruction data indicating first unification instructions, second unification instructions, third unification instructions, and fourth unification instructions; and a processor connected for accessing the memory; the processor accessing the formula data and the unification instruction data and executing the first unification instructions, the second unification instructions, the third unification instructions, and the fourth unification instructions to solve the logical formula; the method comprising: operating the processor to access the unification instruction data and execute the first unification instructions; the processor, in executing the first unification instructions, accessing the formula data in the memory and using the formula data to produce first and second data units and first and second context identifiers and storing the first and second data units and the first and second context identifiers in the memory; the first data unit including the first context identifier and the second data unit including the second context identifier; the first data unit including data relating to linguistic information in a first one of the terms of the logical formula and the second data unit including data relating to linguistic information in a second one of the terms of the logical formula; the first context identifier identifying a first context that includes the respective context of each of a first set of one or more disjuncts of the logical formula; the second context identifier identifying a second context that includes the respective context of each of a second set of one or more disjuncts of the logical formula; the first context applying to the first data unit and the second context applying to the second data unit; operating the processor to access the unification instruction data and execute the second unification instructions; the processor, in executing the second unification instructions, accessing the first data unit and the second data unit and the first and second context identifiers in the memory and using the first and second context identifiers to determine whether to execute the third unification instructions and the fourth unification instructions; operating the processor to access the unification instruction data and execute the third unification instructions; the processor, in executing the third unification instructions, unifying the first and second data units to obtain a unified data unit and storing the unified data unit in the memory; operating the processor to access the unification instruction data and execute the fourth unification instructions; the processor, in executing the fourth unification instructions, accessing the unified data unit in the memory and using the unified data unit to obtain solution data indicating a solution of the logical formula, the solution data including linguistic information about the logical formula.