Methods for mapping over the KB datastructures. The WITH- macros also provide relevant mts for most functions in which the microtheory is an optional argument.

macro **WITH-MT** : (mt &body body)

MT and all its genl mts are relevant within BODY.

macro **WITH-ALL-MTS** : (&body body)

All mts are relevant within BODY.

macro **WITH-JUST-MT** : (mt &body body)

Only MT is relevant within BODY (no genl mts).

macro **WITH-MT-LIST** : (mt-list &body body)

Each mt in the list MT-LIST is relevant within BODY (no genl mts).

macro **WITH-ANY-MT** : (&body body)

Any mt can be used for relevance for a particular inference within &BODY.

macro **WITH-GENL-MTS** : (mt &body body)

MT and all its genl mts are relevant within BODY.

macro **MAP-MTS** : ((var) &body body)

Iterate over all microtheories, binding VAR to an mt and executing BODY.

function **MAP-TERM** : (function term)

Apply FUNCTION to each assertion indexed from TERM.

FUNCTION must satisfy FUNCTION-SPEC-P.

Single value returned satisfies NULL.

function **MAP-TERM-SELECTIVE** : (function term test &optional truth)

Apply FUNCTION to each assertion indexed from TERM with TRUTH that passes TEST.

`If TRUTH is nil, all assertions are mapped.`

FUNCTION must satisfy FUNCTION-SPEC-P.

TEST must satisfy FUNCTION-SPEC-P.

Single value returned satisfies NULL.

function **MAP-TERM-GAFS** : (function term &optional truth)

Apply FUNCTION to every gaf indexed from TERM.

`If TRUTH is nil, all assertions are mapped.`

FUNCTION must satisfy FUNCTION-SPEC-P.

Single value returned satisfies NULL.

function **MAP-MT-CONTENTS** : (function term &optional truth gafs-only)

Apply FUNCTION to each assertion with TRUTH in MT TERM.

`If TRUTH is nil, all assertions are mapped.`

`If GAFS-ONLY, then only gafs are mapped.`

FUNCTION must satisfy FUNCTION-SPEC-P.

Single value returned satisfies NULL.

function **MAP-MT-INDEX** : (function mt &optional truth gafs-only)

Apply FUNCTION to each assertion with TRUTH at mt index MT.

`If TRUTH is nil, all assertions are mapped.`

`If GAFS-ONLY, then only gafs are mapped.`

FUNCTION must satisfy FUNCTION-SPEC-P.

Single value returned satisfies NULL.

function **MAP-OTHER-INDEX** : (function term &optional truth gafs-only)

Apply FUNCTION to each assertion with TRUTH at other index TERM.

`If TRUTH is nil, all assertions are mapped.`

`If GAFS-ONLY, then only gafs are mapped.`

FUNCTION must satisfy FUNCTION-SPEC-P.

Single value returned satisfies NULL.

function **GATHER-INDEX** : (term &optional remove-duplicates?)

Return a list of all mt-relevant assertions indexed via TERM.

If REMOVE-DUPLICATES? is non-nil, assertions are guaranteed to only be listed once.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-INDEX-IN-ANY-MT** : (term &optional remove-duplicates?)

Return a list of all assertions indexed via TERM.

If REMOVE-DUPLICATES? is non-nil, assertions are guaranteed to only be listed once.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-EXCEPTION-RULE-INDEX** : (rule &optional mt direction)

Return a list of all non-gaf assertions (rules) such that:

a) it has a positive literal of the form (abnormal <whatever> RULE)

b) if MT is non-nil, then MT must be its microtheory

c) if DIRECTION is non-nil, then DIRECTION must be its direction.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-FUNCTION-EXTENT-INDEX** : (func)

Return a list of all #$termOfUnit assertions such that:

FUNC is the functor of the naut arg2.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-FUNCTION-RULE-INDEX** : (func &optional mt direction)

Return a list of all non-gaf assertions (rules) such that:

a) it has a negative literal of the form (termOfUnit <whatever> (FUNC . <whatever>))

b) if MT is non-nil, then MT must be its microtheory

c) if DIRECTION is non-nil, then DIRECTION must be its direction.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-GAF-ARG-INDEX** : (term argnum &optional pred mt truth)

Return a list of all gaf assertions such that:

a) TERM is its ARGNUMth argument

b) if TRUTH is non-nil, then TRUTH is its truth value

c) if PRED is non-nil, then PRED must be its predicate

d) if MT is non-nil, then MT must be its microtheory (and PRED must be non-nil).

ARGNUM must satisfy POSITIVE-INTEGER-P.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-GENL-MT-RULE-INDEX** : (genl-mt sense &optional rule-mt direction)

Return a list of all non-gaf assertions (rules) such that:

a) if SENSE is :pos, it has a positive literal of the form (genlMt <whatever> GENL-MT)

b) if SENSE is :neg, it has a negative literal of the form (genlMt <whatever> GENL-MT)

c) if RULE-MT is non-nil, then RULE-MT must be its microtheory

d) if DIRECTION is non-nil, then DIRECTION must be its direction.

SENSE must satisfy SENSE-P.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-GENLS-RULE-INDEX** : (collection sense &optional mt direction)

Return a list of all non-gaf assertions (rules) such that:

a) if SENSE is :pos, it has a positive literal of the form (genls <whatever> COLLECTION)

b) if SENSE is :neg, it has a negative literal of the form (genls <whatever> COLLECTION)

c) if MT is non-nil, then MT must be its microtheory

d) if DIRECTION is non-nil, then DIRECTION must be its direction.

SENSE must satisfy SENSE-P.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-ISA-RULE-INDEX** : (collection sense &optional mt direction)

Return a list of all non-gaf assertions (rules) such that:

a) if SENSE is :pos, it has a positive literal of the form (isa <whatever> COLLECTION)

b) if SENSE is :neg, it has a negative literal of the form (isa <whatever> COLLECTION)

c) if MT is non-nil, then MT must be its microtheory

d) if DIRECTION is non-nil, then DIRECTION must be its direction.

SENSE must satisfy SENSE-P.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-MT-INDEX** : (term)

Return a list of all assertions such that TERM is its microtheory.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-NART-ARG-INDEX** : (term argnum &optional func)

Return a list of all #$termOfUnit assertions with a naut arg2 such that:

a) TERM is its ARGNUMth argument

b) if FUNC is non-nil, then FUNC must be its functor

ARGNUM must satisfy POSITIVE-INTEGER-P.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-OTHER-INDEX** : (term)

Return a list of other assertions mentioning TERM but not indexed in any other more useful manner.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-PREDICATE-EXTENT-INDEX** : (pred &optional mt truth)

Return a list of all gaf assertions such that:

a) PRED is its predicate

b) if TRUTH is non-nil, then TRUTH is its truth value

c) if MT is non-nil, then MT must be its microtheory.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-PREDICATE-RULE-INDEX** : (pred sense &optional mt direction)

Return a list of all non-gaf assertions (rules) such that:

a) if SENSE is :pos, it has PRED as a predicate in a positive literal

b) if SENSE is :neg, it has PRED as a predicate in a negative literal

c) if MT is non-nil, then MT must be its microtheory

d) if DIRECTION is non-nil, then DIRECTION must be its direction.

SENSE must satisfy SENSE-P.

Single value returned is a list of elements satisfying ASSERTION-P.

function **GATHER-TERM-ASSERTIONS** : (term &optional mt)

Return a list of all mt-relevant assertions of TERM.

Single value returned is a list of elements satisfying ASSERTION-P.

function **FPRED-VALUE** : (term pred &optional index-arg gather-arg truth)

Find the first gaf assertion such that:

`(a) the assertion is in a relevant microtheory (relevance is established outside)`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return the term in the GATHER-ARG position if such an assertion exists.`

`Otherwise, return NIL.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies HL-TERM-P or is NIL.

function **FPRED-VALUE-IN-MT** : (term pred mt &optional index-arg gather-arg truth)

Find the first gaf assertion such that:

`(a) the assertion is in microtheory MT`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return the term in the GATHER-ARG position if such an assertion exists.`

`Otherwise, return NIL.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

MT must satisfy HLMT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies HL-TERM-P or is NIL.

function **FPRED-VALUE-IN-MTS** : (term pred mts &optional index-arg gather-arg truth)

Find the first gaf assertion such that:

`(a) the assertion is in one of the microtheories in the list MTS`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return the term in the GATHER-ARG position if such an assertion exists.`

`Otherwise, return NIL.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

MTS must satisfy LISTP.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies HL-TERM-P or is NIL.

function **FPRED-VALUE-IN-ANY-MT** : (term pred &optional index-arg gather-arg truth)

Find the first gaf assertion such that:

`(a) the assertion is allowed to be in any microtheory`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return the term in the GATHER-ARG position if such an assertion exists.`

`Otherwise, return NIL.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies HL-TERM-P or is NIL.

function **FPRED-VALUE-IN-RELEVANT-MTS** : (term pred &optional mt index-arg gather-arg truth)

If MT is NIL, behaves like FPRED-VALUE. Otherwise, behaves like FPRED-VALUE-IN-MT.

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies HL-TERM-P or is NIL.

function **PRED-VALUES** : (term pred &optional index-arg gather-arg truth)

Find all gaf assertions such that:

`(a) the assertion is in a relevant microtheory (relevance is established outside)`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return a list of the terms in the GATHER-ARG position of all such assertions.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying HL-TERM-P.

function **PRED-VALUES-IN-MT** : (term pred mt &optional index-arg gather-arg truth)

Find all gaf assertions such that:

`(a) the assertion is in microtheory MT`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return a list of the terms in the GATHER-ARG position of all such assertions.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

MT must satisfy HLMT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying HL-TERM-P.

function **PRED-VALUES-IN-MTS** : (term pred mts &optional index-arg gather-arg truth)

Find all gaf assertions such that:

`(a) the assertion is in one of the microtheories in the list MTS`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return a list of the terms in the GATHER-ARG position of all such assertions.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

MTS must satisfy LISTP.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying HL-TERM-P.

function **PRED-VALUES-IN-ANY-MT** : (term pred &optional index-arg gather-arg truth)

Find all gaf assertions such that:

`(a) the assertion is allowed to be in any microtheory`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return a list of the terms in the GATHER-ARG position of all such assertions.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying HL-TERM-P.

function **PRED-VALUES-IN-RELEVANT-MTS** : (term pred &optional mt index-arg gather-arg truth)

If MT is NIL, behaves like PRED-VALUES. Otherwise, behaves like PRED-VALUES-IN-MT

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying HL-TERM-P.

function **PRED-REFS** : (pred &optional gather-arg truth)

Find all gaf assertions such that:

`(a) the assertion is in a relevant microtheory (relevance is established outside)`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`Return a list of the terms in the GATHER-ARG position of all such assertions.`

PRED must satisfy FORT-P.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying HL-TERM-P.

function **PRED-REFS-IN-MT** : (pred mt &optional gather-arg truth)

Find all gaf assertions such that:

`(a) the assertion is in microtheory MT`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`Return a list of the terms in the GATHER-ARG position of all such assertions.`

PRED must satisfy FORT-P.

MT must satisfy HLMT-P.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying HL-TERM-P.

function **PRED-REFS-IN-MTS** : (pred mts &optional gather-arg truth)

Find all gaf assertions such that:

`(a) the assertion is in one of the microtheories in the list MTS`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`Return a list of the terms in the GATHER-ARG position of all such assertions.`

PRED must satisfy FORT-P.

MTS must satisfy LISTP.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying HL-TERM-P.

function **PRED-REFS-IN-ANY-MT** : (pred &optional gather-arg truth)

Find all gaf assertions such that:

`(a) the assertion is allowed to be in any microtheory`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`Return a list of the terms in the GATHER-ARG position of all such assertions.`

PRED must satisfy FORT-P.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying HL-TERM-P.

function **PRED-REFS-IN-RELEVANT-MTS** : (pred &optional mt gather-arg truth)

If MT is NIL, behaves like PRED-REFS. Otherwise, behaves like PRED-REFS-IN-MT

PRED must satisfy FORT-P.

GATHER-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying HL-TERM-P.

function **SOME-PRED-VALUE** : (term pred &optional index-arg truth)

Find the first gaf assertion such that:

`(a) the assertion is in a relevant microtheory (relevance is established outside)`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return T if such an assertion exists, otherwise return NIL.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies BOOLEANP.

function **SOME-PRED-VALUE-IN-MT** : (term pred mt &optional index-arg truth)

Find the first gaf assertion such that:

`(a) the assertion is in microtheory MT`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return T if such an assertion exists, otherwise return NIL.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

MT must satisfy HLMT-P.

INDEX-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies BOOLEANP.

function **SOME-PRED-VALUE-IN-MTS** : (term pred mts &optional index-arg truth)

Find the first gaf assertion such that:

`(a) the assertion is in one of the microtheories in the list MTS`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return T if such an assertion exists, otherwise return NIL.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

MTS must satisfy LISTP.

INDEX-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies BOOLEANP.

function **SOME-PRED-VALUE-IN-ANY-MT** : (term pred &optional index-arg truth)

Find the first gaf assertion such that:

`(a) the assertion is allowed to be in any microtheory`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return T if such an assertion exists, otherwise return NIL.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies BOOLEANP.

function **SOME-PRED-VALUE-IN-RELEVANT-MTS** : (term pred &optional mt index-arg truth)

If MT is NIL, behaves like SOME-PRED-VALUE. Otherwise, behaves like SOME-PRED-VALUE-IN-MT

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies BOOLEANP.

function **PRED-U-V-HOLDS** : (pred u v &optional u-arg v-arg truth)

Find the first gaf assertion such that:

`(a) the assertion is in a relevant microtheory (relevance is established outside)`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) U is the term in the U-ARG position.`

`(e) V is the term in the V-ARG position.`

`Return T if such an assertion exists, otherwise return NIL.`

PRED must satisfy FORT-P.

U must satisfy INDEXED-TERM-P.

V must satisfy HL-TERM-P.

U-ARG must satisfy INTEGERP.

V-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies BOOLEANP.

function **PRED-U-V-HOLDS-IN-MT** : (pred u v mt &optional u-arg v-arg truth)

Find the first gaf assertion such that:

`(a) the assertion is in microtheory MT`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) U is the term in the U-ARG position.`

`(e) V is the term in the V-ARG position.`

`Return T if such an assertion exists, otherwise return NIL.`

PRED must satisfy FORT-P.

U must satisfy INDEXED-TERM-P.

V must satisfy HL-TERM-P.

MT must satisfy HLMT-P.

U-ARG must satisfy INTEGERP.

V-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies BOOLEANP.

function **PRED-U-V-HOLDS-IN-MTS** : (pred u v mts &optional u-arg v-arg truth)

Find the first gaf assertion such that:

`(a) the assertion is in one of the microtheories in the list MTS`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) U is the term in the U-ARG position.`

`(e) V is the term in the V-ARG position.`

`Return T if such an assertion exists, otherwise return NIL.`

PRED must satisfy FORT-P.

U must satisfy INDEXED-TERM-P.

V must satisfy HL-TERM-P.

MTS must satisfy LISTP.

U-ARG must satisfy INTEGERP.

V-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies BOOLEANP.

function **PRED-U-V-HOLDS-IN-ANY-MT** : (pred u v &optional u-arg v-arg truth)

Find the first gaf assertion such that:

`(a) the assertion is allowed to be in any microtheory`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) U is the term in the U-ARG position.`

`(e) V is the term in the V-ARG position.`

`Return T if such an assertion exists, otherwise return NIL.`

PRED must satisfy FORT-P.

U must satisfy INDEXED-TERM-P.

V must satisfy HL-TERM-P.

U-ARG must satisfy INTEGERP.

V-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies BOOLEANP.

function **PRED-U-V-HOLDS-IN-RELEVANT-MTS** : (pred u v &optional mt u-arg v-arg truth)

If MT is NIL, behaves like PRED-U-V-HOLDS. Otherwise, behaves like PRED-U-V-HOLDS-IN-MT

PRED must satisfy FORT-P.

U must satisfy INDEXED-TERM-P.

V must satisfy HL-TERM-P.

U-ARG must satisfy INTEGERP.

V-ARG must satisfy INTEGERP.

TRUTH must satisfy TRUTH-P.

Single value returned satisfies BOOLEANP.

function **PRED-VALUE-TUPLES** : (term pred index-arg gather-args &optional truth)

Find all gaf assertions such that:

`(a) the assertion is in a relevant microtheory (relevance is established outside)`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return a list of tuples formed from the GATHER-ARGS positions of all such assertions.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARGS must satisfy LISTP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying LISTP.

function **PRED-VALUE-TUPLES-IN-MT** : (term pred index-arg gather-args mt &optional truth)

Find all gaf assertions such that:

`(a) the assertion is microtheory MT`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return a list of tuples formed from the GATHER-ARGS positions of all such assertions.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARGS must satisfy LISTP.

MT must satisfy HLMT-P.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying LISTP.

function **PRED-VALUE-TUPLES-IN-MTS** : (term pred index-arg gather-args mts &optional truth)

Find all gaf assertions such that:

`(a) the assertion is in one of the microtheories in the list MTS`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return a list of tuples formed from the GATHER-ARGS positions of all such assertions.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARGS must satisfy LISTP.

MTS must satisfy LISTP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying LISTP.

function **PRED-VALUE-TUPLES-IN-ANY-MT** : (term pred index-arg gather-args &optional truth)

Find all gaf assertions such that:

`(a) the assertion is allowed to be from any microtheory`

`(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value`

`(c) PRED is the predicate used.`

`(d) TERM is the term in the INDEX-ARG position.`

`Return a list of tuples formed from the GATHER-ARGS positions of all such assertions.`

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARGS must satisfy LISTP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying LISTP.

function **PRED-VALUE-TUPLES-IN-RELEVANT-MTS** : (term pred index-arg gather-args &optional mt truth)

If MT is NIL, behaves like PRED-VALUE-TUPLES. Otherwise, behaves like PRED-VALUE-TUPLES-IN-MT

TERM must satisfy INDEXED-TERM-P.

PRED must satisfy FORT-P.

INDEX-ARG must satisfy INTEGERP.

GATHER-ARGS must satisfy LISTP.

TRUTH must satisfy TRUTH-P.

Single value returned is a list of elements satisfying LISTP.

KB Indexing | Home | KB Accessors |