Formalized Common Knowledge
           
             

Home

Projects

FAQ

Documentation

Releases

Downloads

Discussion

News

License

Wiki

   printable version

The OpenCyc SubL Application Programming Interface
(OpenCyc SubL API, a.k.a. Cyc API)


February 25, 2002
Version 1.0

Copyright 1997 - 2003 Cycorp, Inc.

OpenCyc.org

OpenCyc at SourceForge

THIS SOFTWARE AND KNOWLEDGE BASE CONTENT ARE PROVIDED ``AS IS'' AND ANY EXPRESSED OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE OPENCYC ORGANIZATION OR ITS CONTRIBUTORS, OR CYCORP INC. BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE AND KNOWLEDGE BASE CONTENT, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

1. Introduction

This document describes the Cyc Application Programmers Interface (API). This is the protocol which allows applications to connect to and use the various CycL modules and functionality which together are used to maintain the Cyc Knowledge Base.

The Cyc API is divided into two layers :

  • The Content Layer categorizes the available functions, and provides the function signatures and documentation used by applications. The java CycAccess class contains the majority of these functions for ease of integration.
  • The Transport Layer establishes connection to a Cyc server and performs the message handling. The ASCII telnet connection is useful for debugging and remote administration, and the binary CFASL interface is used for applications. The java CycConnection, CfaslInputStream and CfaslOutputStream classes contain the transport layer functions.

2. Content Layer

The Content Layer of the Cyc API contains a list of the exposed functionality provided by the Cyc server. Each category is described below, followed by a list of the function signatures and documentation. Appendix A provides an Index of all functions in the Content Layer.

Cycorp has implemented the Cyc API in a language it designed called SubL. SubL in turn can be easily implemented in both Common Lisp and C, and can therefore be -- and has been -- ported to many different platforms and operating systems. The function and macro signatures are given in SubL format, which in this case is identical to Common Lisp format. For more on SubL, see the SubL Reference manual.

Contents

2.1.1

Constants

2.1.2

NATS (Non Atomic Terms)

2.1.3

FORTS (First Order Reified Terms)

2.1.4

HL Assertions

2.1.5

HL Formulas and Clauses

2.1.6

HL Arguments

2.1.7

HL Deductions

2.1.8

HL Supports

2.1.9

HL Variables

2.2

KB Indexing

2.3

KB Mapping

2.4

KB Accessors

2.5

Epistemological-Level Support

2.6

Transitivity HL Modules

2.6.1

Subsumption-Based HL Modules

2.6.1.1

#$isa support

2.6.1.2

#$genls support

2.6.1.3

#$genlPreds and #$genlInverse support

2.6.1.4

General Transitivity support

2.6.1.5

#$genlAttributes support

2.7

Inference Module

Appendix A : Glossary

Appendix B : Index

2.1 KB representation

Methods for directly manipulating KB datastructures

2.1.1 Constants

function CONSTANT-P : (object)
Return T iff the argument is a CycL constant
Single value returned satisfies BOOLEANP.

function CONSTANT-EXTERNAL-ID : (constant)
Return the external id of CONSTANT.
CONSTANT must satisfy CONSTANT-P.
Single value returned satisfies CONSTANT-EXTERNAL-ID-P or is NIL.

function CONSTANT-INTERNAL-ID : (constant)
Return the internal id of CONSTANT.
CONSTANT must satisfy CONSTANT-P.
Single value returned satisfies CONSTANT-INTERNAL-ID-P or is NIL.

function CONSTANT-NAME : (constant)
Return the name of CONSTANT or :unnamed.
CONSTANT must satisfy CONSTANT-P.

function FIND-CONSTANT : (name)
Return the constant with NAME, or NIL if not present.
NAME must satisfy STRINGP.
Single value returned satisfies CONSTANT-P or is NIL.

function FIND-CONSTANT-BY-EXTERNAL-ID : (external-id)
Return the constant with EXTERNAL-ID, or NIL if not present.
EXTERNAL-ID must satisfy CONSTANT-EXTERNAL-ID-P.
Single value returned satisfies CONSTANT-P or is NIL.

function FIND-CONSTANT-BY-INTERNAL-ID : (id)
Return the constant with internal ID, or NIL if not present.
ID must satisfy CONSTANT-INTERNAL-ID-P.
Single value returned satisfies CONSTANT-P or is NIL.

function CREATE-CONSTANT : (name &optional external-id)
Return a new constant named NAME. Use EXTERNAL-ID if non-null, else create a new ID.
Single value returned satisfies CONSTANT-P.

function FIND-OR-CREATE-CONSTANT : (name &optional external-id)
Return the constant with NAME if it exists, otherwise create it with EXTERNAL-ID.
Also, if it exists but has a null id, install EXTERNAL-ID on the constant.
NAME must satisfy STRINGP.
Single value returned satisfies CONSTANT-P.

function RENAME-CONSTANT : (constant new-name)
Rename CONSTANT to have NEW-NAME as its name. The constant is returned.
CONSTANT must satisfy CONSTANT-P.
NEW-NAME must satisfy STRINGP.
Single value returned satisfies CONSTANT-P.

function UNIQUIFY-CONSTANT-NAME : (name)
Return a unique, currently unused constant name based on NAME, which must be a valid constant name.
NAME must satisfy STRINGP.
Single value returned satisfies STRINGP.

function REMOVE-CONSTANT : (constant)
Remove constant from the KB.
CONSTANT must satisfy CONSTANT-P.
Single value returned satisfies NULL.

macro DO-CONSTANTS : ((var &optional (message "mapping Cyc constants")) &body body)
Iterate over all HL constant datastructures, executing BODY within the scope of VAR.
VAR is bound to each constant in turn.
MESSAGE is a progress message string.

function CONSTANT-COUNT : ()
Return the total number of constants.
Single value returned satisfies INTEGERP.

function VALID-CONSTANT-NAME-CHAR : (char)
Return T iff CHAR is a character which is allowed in a valid constant name.
CHAR must satisfy CHARACTERP.
Single value returned satisfies BOOLEANP.

function VALID-CONSTANT-NAME : (string)
Return T iff STRING is a valid name for a constant.
Single value returned satisfies BOOLEANP.

function CONSTANT-COMPLETE-EXACT : (string &optional start end)
Return a valid constant whose name exactly matches STRING.
Optionally the START and END character positions can be
specified, such that the STRING matches characters between the START and
END range. If no constant exists, return NIL.
STRING must satisfy STRINGP.
START must satisfy FIXNUMP.

function CONSTANT-COMPLETE : (prefix &optional case-sensitive? exact-length? start end)
Return all valid constants with PREFIX as a prefix of their name
When CASE-SENSITIVE? is non-nil, the comparison is done in a case-sensitive fashion.
When EXACT-LENGTH? is non-nil, the prefix must be the entire string
Optionally the START and END character positions can be
specified, such that the PREFIX matches characters between the START and
END range. If no constant exists, return NIL.
PREFIX must satisfy STRINGP.
CASE-SENSITIVE? must satisfy BOOLEANP.
EXACT-LENGTH? must satisfy BOOLEANP.
START must satisfy FIXNUMP.

function CONSTANT-APROPOS : (substring &optional case-sensitive? start end)
Return all valid constants with SUBSTRING somewhere in their name
When CASE-SENSITIVE? is non-nil, the comparison is done in a case-sensitive fashion.
Optionally the START and END character positions can be
specified, such that the SUBSTRING matches characters between the START and
END range. If no constant exists, return NIL.
SUBSTRING must satisfy STRINGP.
CASE-SENSITIVE? must satisfy BOOLEANP.
START must satisfy FIXNUMP.

2.1.2 NARTS (Non Atomic Reified Terms)

function NART-P : (object)
Return T iff OBJECT is a datastructure implementing a non-atomic reified term (NART).
Single value returned satisfies BOOLEANP.

function NART-ID : (nart)
Return the id of this NART.
NART must satisfy NART-P.
Single value returned satisfies INTEGERP.

function FIND-NART-BY-ID : (id)
Return the NART with ID, or NIL if not present.
ID must satisfy INTEGERP.
Single value returned satisfies NART-P or is NIL.

function NART-HL-FORMULA : (nart)
Return the hl formula of this NART.
NART must satisfy NART-P.
Single value returned satisfies CONSP or is NIL.

function NART-EL-FORMULA : (nart)
Return the el formula of this NART.
NART must satisfy NART-P.
Single value returned satisfies CONSP or is NIL.

function REMOVE-NART : (nart)
Remove NART from the KB.
NART must satisfy NART-P.
Single value returned satisfies NULL.

function NART-COUNT : ()
Return the total number of NARTs.
Single value returned satisfies INTEGERP.

macro DO-NARTS : ((var &optional (message "mapping Cyc NARTs")) &body body)
Iterate over all HL NART datastructures, executing BODY within the scope of VAR.
VAR is bound to the NART.
MESSAGE is a progress message string.

2.1.3 FORTS

function FORT-P : (object)
Return T iff OBJECT is a first order reified term (FORT).
Single value returned satisfies BOOLEANP.

function EL-FORT-P : (object)
Returns t iff OBJECT is a fort or an EL formula.
Single value returned satisfies BOOLEANP.

function FORT-EL-FORMULA : (fort)
Return the EL formula for any FORT.
FORT must satisfy FORT-P.
Single value returned satisfies CONSP or is NIL.

function REMOVE-FORT : (fort)
Remove FORT from the KB.
FORT must satisfy FORT-P.
Single value returned satisfies NULL.

function FORT-COUNT : ()
Return the total number of FORTs.
Single value returned satisfies INTEGERP.

macro DO-FORTS : ((var &optional (message "mapping Cyc FORTs")) &body body)
Iterate over all HL FORT datastructures, executing BODY within the scope of VAR.
VAR is bound to the FORT.
MESSAGE is a progress message string.

2.1.4 HL Assertions

function ASSERTION-P : (object)
Return T iff OBJECT is an HL assertion
Single value returned satisfies BOOLEANP.

function ASSERTION-ID : (assertion)
Return the id of this ASSERTION.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies INTEGERP.

function ASSERTION-CNF : (assertion)
Return the cnf of ASSERTION.
@note If you know the assertion is a gaf,
consider using gaf-formula instead,
if you do not explicitly need a CNF.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies CNF-P.

function ASSERTION-FORMULA : (assertion)
Return a formula for ASSERTION.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies EL-FORMULA-P.

function ASSERTION-IST-FORMULA : (assertion)
Return a formula in #$ist format for ASSERTION.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies EL-FORMULA-P.

function ASSERTION-MENTIONS-TERM : (assertion term)
Return T iff ASSERTION's formula or mt contains TERM.
If assertion is a meta-assertion, recurse down sub-assertions.
By convention, negated gafs do not necessarily mention the term #$not.
ASSERTION must satisfy ASSERTION-P.
TERM must satisfy HL-TERM-P.
Single value returned satisfies BOOLEANP.

function ASSERTION-MT : (assertion)
Return the mt of ASSERTION.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies FORT-P.

function ASSERTION-DIRECTION : (assertion)
Return the direction of ASSERTION (either :backward, :forward or :code).
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies DIRECTION-P.

function FORWARD-ASSERTION? : (assertion)
Predicate returns T iff ASSERTION's direction is :FORWARD.
Single value returned satisfies BOOLEANP.

function BACKWARD-ASSERTION? : (assertion)
Predicate returns T iff ASSERTION's direction is :BACKWARD.
Single value returned satisfies BOOLEANP.

function DIRECTION-P : (object)
Return T iff OBJECT is a valid assertion inference direction
:backward :forward or :code.
Single value returned satisfies BOOLEANP.

function CODE-ASSERTION? : (assertion)
Predicate returns T iff ASSERTION's direction is :CODE.
Single value returned satisfies BOOLEANP.

function ASSERTION-TRUTH : (assertion)
Return the current truth of ASSERTION -- either :true :false or :unknown.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies TRUTH-P.

function ASSERTION-HAS-TRUTH : (assertion truth)
Return T iff ASSERTION's current truth is TRUTH.
ASSERTION must satisfy ASSERTION-P.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies BOOLEANP.

function TRUTH-P : (object)
Returns T iff OBJECT is a valid CycL truth
:true :false or :unknown.

function ASSERTION-STRENGTH : (assertion)
Return the current argumentation strength of ASSERTION -- either :monotonic :default or :unknown.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies EL-STRENGTH-P.

function ASSERTION-HAS-META-ASSERTIONS? : (assertion)
Return T iff ASSERTION has some meta-assertions.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies BOOLEANP.

function FIND-ASSERTION-BY-ID : (id)
Return the assertion with ID, or NIL if not present.
ID must satisfy INTEGERP.
Single value returned satisfies ASSERTION-P or is NIL.

function FIND-ASSERTION : (cnf mt)
Find the assertion in MT with CNF. Return NIL if not present.
CNF must satisfy CNF-P.
MT must satisfy FORT-P.
Single value returned satisfies ASSERTION-P or is NIL.

function FIND-ASSERTION-ANY-MT : (cnf)
Find any assertion in any mt with CNF. Return NIL if none are present.
CNF must satisfy CNF-P.
Single value returned satisfies ASSERTION-P or is NIL.

function FIND-ALL-ASSERTIONS : (cnf)
Return all assertions that have CNF or NIL if there aren't any.
CNF must satisfy CNF-P.
Single value returned satisfies (LIST ASSERTION-P) or is NIL.

function FIND-GAF : (gaf mt)
Find the assertion in MT with GAF as its formula. Return NIL if not present.
GAF must satisfy EL-FORMULA-P.
MT must satisfy FORT-P.
Single value returned satisfies ASSERTION-P or is NIL.

function FIND-GAF-ANY-MT : (gaf)
Find any assertion in any mt with GAF as its formula. Return NIL if not present.
GAF must satisfy EL-FORMULA-P.
Single value returned satisfies ASSERTION-P or is NIL.

function FIND-ALL-GAFS : (gaf)
Return all assertions of GAF or NIL if there aren't any.
GAF must satisfy EL-FORMULA-P.
Single value returned satisfies (LIST ASSERTION-P) or is NIL.

function GET-ASSERTED-ARGUMENT : (assertion)
Return the asserted argument for ASSERTION, or nil if none present.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies ASSERTED-ARGUMENT-P or is NIL.

function ASSERTED-ASSERTION? : (assertion)
Return non-nil IFF assertion has an asserted argument.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies BOOLEANP.

function DEDUCED-ASSERTION? : (assertion)
Return non-nil IFF assertion has some deduced argument
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies BOOLEANP.

function ASSERTION-EL-IST-FORMULA : (assertion)
Return the el formula in #$ist format for ASSERTION.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies CONSP.

function ASSERTION-HAS-DEPENDENTS-P : (assertion)
Return non-nil IFF assertion has dependents.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies BOOLEANP.

macro DO-ASSERTIONS : ((var &optional (message "mapping Cyc assertions")) &body body)
Iterate over all HL assertion datastructures, executing BODY within the scope of VAR.
VAR is bound to the assertion.
MESSAGE is a progress message string.

function ASSERTION-COUNT : ()
Return the total number of assertions.
Single value returned satisfies INTEGERP.

2.1.5 HL Formulas and Clauses

function NEGATED? : (form)
Assuming FORM is a valid CycL formula, return T IFF it is negated.
FORM must satisfy EL-FORMULA-P.
Single value returned satisfies BOOLEANP.

function NEGATE : (form)
Assuming FORM is a valid CycL formula, return a negated version of it.
FORM must satisfy EL-FORMULA-P.
Single value returned satisfies EL-FORMULA-P.

function CLAUSE-P : (object)
Returns T iff OBJECT is either a CNF or DNF clause.
Single value returned satisfies BOOLEANP.

function SENSE-P : (object)
Return T iff OBJECT is a valid CycL literal sense
:neg or :pos.
Single value returned satisfies BOOLEANP.

function MAKE-CLAUSE : (neg-lits pos-lits)
Construct a clause from NEG-LITS and POS-LITS, each of which are lists of literals.
NEG-LITS must satisfy LISTP.
POS-LITS must satisfy LISTP.
Single value returned satisfies CLAUSE-P.

function NEG-LITS : (clause)
Return the neg-lits of CLAUSE.
CLAUSE must satisfy CLAUSE-P.
Single value returned satisfies LISTP.

function POS-LITS : (clause)
Return the pos-lits of CLAUSE.
CLAUSE must satisfy CLAUSE-P.
Single value returned satisfies LISTP.

function CLAUSE-EQUAL : (clause1 clause2)
Return T iff CLAUSE1 and CLAUSE2 are both equivalent clauses.
Single value returned satisfies BOOLEANP.

function EMPTY-CLAUSE : ()
Return the empty clause.
Single value returned satisfies CLAUSE-P.

function EMPTY-CLAUSE? : (clause)
Return T iff CLAUSE is empty.
CLAUSE must satisfy CLAUSE-P.
Single value returned satisfies BOOLEANP.

function CLAUSE-LITERAL : (clause sense num)
Return literal in CLAUSE specified by SENSE and NUM.
SENSE must be either :pos or :neg.
CLAUSE must satisfy CLAUSE-P.
SENSE must satisfy SENSE-P.
NUM must satisfy INTEGERP.

function CLAUSE-WITHOUT-LITERAL : (clause sense num)
Return a new clause which is CLAUSE without the literal specified by SENSE and NUM.
SENSE must be either :pos or :neg.
CLAUSE must satisfy CLAUSE-P.
SENSE must satisfy SENSE-P.
NUM must satisfy INTEGERP.
Single value returned satisfies CLAUSE-P.

function GROUND-CLAUSE-P : (clause)
Return T iff CLAUSE is a ground clause.
Single value returned satisfies BOOLEANP.

function CNF-P : (object)
Returns T iff OBJECT is a canonicalized CycL formula in conjunctive normal form.
Single value returned satisfies BOOLEANP.

function GAF-CNF? : (cnf)
Return T iff CNF is a cnf representation of a gaf formula.
Single value returned satisfies BOOLEANP.

function CNF-FORMULA : (cnf &optional truth)
Return a readable formula of CNF
TRUTH only gets looked at for ground, single pos lit cnfs
in which case TRUTH gives the truth of the gaf.
CNF must satisfy CNF-P.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies EL-FORMULA-P.

function CNF-FORMULA-FROM-CLAUSES : (cnf-clauses)
Return a readable formula from a list of CNF-CLAUSES.
CNF-CLAUSES must satisfy LISTP.
Single value returned satisfies EL-FORMULA-P.

function DNF-FORMULA : (dnf)
Return a readable formula of DNF.
Single value returned satisfies EL-FORMULA-P.

function DNF-FORMULA-FROM-CLAUSES : (dnf-clauses)
Return a readable formula from a list of DNF-CLAUSES.
DNF-CLAUSES must satisfy LISTP.
Single value returned satisfies EL-FORMULA-P.

function ATOMIC-CLAUSE-P : (clause)
Return T iff CLAUSE is an atomic clause.
Single value returned satisfies BOOLEANP.

function HL-TERM-P : (obj)
Returns T if the OBJ is a valid CycL HL term.
Single value returned satisfies BOOLEANP.

2.1.6 HL Arguments

function HL-MODULE-P : (object)
Return T iff OBJECT is an HL module.
Single value returned satisfies BOOLEANP.

function ARGUMENT-P : (object)
Return T iff OBJECT is an HL argument structure.
Single value returned satisfies BOOLEANP.

function ASSERTED-ARGUMENT-P : (object)
Return T iff OBJECT is an HL asserted argument structure.
Single value returned satisfies BOOLEANP.

function ARGUMENT-EQUAL : (argument1 argument2)
Return T iff ARGUMENT1 and ARGUMENT2 are equivalent arguments.
Single value returned satisfies BOOLEANP.

function ARGUMENT-TRUTH : (argument)
Return the truth of ARGUMENT.
ARGUMENT must satisfy ARGUMENT-P.

function ARGUMENT-STRENGTH : (argument)
Return the strength of ARGUMENT.
ARGUMENT must satisfy ARGUMENT-P.

2.1.7 HL Deductions

function DEDUCTION-P : (object)
Return T iff OBJECT is a CycL deduction.
Single value returned satisfies BOOLEANP.

function DEDUCTION-ID : (deduction)
Return the id of DEDUCTION.
DEDUCTION must satisfy DEDUCTION-P.
Single value returned satisfies INTEGERP.

function FIND-DEDUCTION-BY-ID : (id)
Return the deduction with ID, or NIL if not present.
ID must satisfy INTEGERP.
Single value returned satisfies DEDUCTION-P or is NIL.

function DEDUCTION-ASSERTION : (deduction)
Return the assertion for which DEDUCTION is a deduction.
DEDUCTION must satisfy DEDUCTION-P.
Single value returned satisfies ASSERTION-P.

function DEDUCTION-COUNT : ()
Return the total number of deductions.
Single value returned satisfies INTEGERP.

macro DO-DEDUCTIONS : ((var &optional (message "mapping Cyc deductions")) &body body)
Iterate over all HL deduction datastructures, executing BODY within the scope of VAR.
VAR is a deduction.
MESSAGE is a progress message string.

2.1.8 HL Supports

function SUPPORT-P : (object)
Return T iff OBJECT can be a support in an argument.
Single value returned satisfies BOOLEANP.

function SUPPORT-MODULE : (support)
Return the module of SUPPORT.
SUPPORT must satisfy SUPPORT-P.
Single value returned satisfies HL-MODULE-P.

function SUPPORT-MT : (support)
Return the microtheory of SUPPORT.
SUPPORT must satisfy SUPPORT-P.
Single value returned satisfies FORT-P.

function SUPPORT-TRUTH : (support)
Return the truth of SUPPORT.
SUPPORT must satisfy SUPPORT-P.
Single value returned satisfies TRUTH-P.

function SUPPORT-STRENGTH : (support)
Return the strength of SUPPORT.
SUPPORT must satisfy SUPPORT-P.
Single value returned satisfies EL-STRENGTH-P.

function SUPPORT-SENTENCE : (support)
Return the sentence of SUPPORT.
SUPPORT must satisfy SUPPORT-P.
Single value returned satisfies CONSP.

function HL-SUPPORT-P : (object)
Does OBJECT represent an HL support?
Single value returned satisfies BOOLEANP.

function MAKE-HL-SUPPORT : (hl-module sentence &optional mt tv)
Construct a new HL support.
HL-MODULE must satisfy HL-MODULE-P.
SENTENCE must satisfy POSSIBLY-SENTENCE-P.
MT must satisfy FORT-P.
TV must satisfy TV-P.
Single value returned satisfies HL-SUPPORT-P.

2.1.9 HL Variables

function EL-VAR? : (object)
Return T iff OBJECT is a symbol which can be interpreted as an EL variable.
Single value returned satisfies BOOLEANP.

function VARIABLE-P : (object)
Return T iff OBJECT is an HL variable.
Single value returned satisfies BOOLEANP.

function FIND-VARIABLE-BY-ID : (id)
Return the HL variable with ID, or NIL if not present.
ID must satisfy INTEGERP.
Single value returned satisfies VARIABLE-P or is NIL.

function VARIABLE-ID : (variable)
Return id of HL variable VARIABLE.
VARIABLE must satisfy VARIABLE-P.
Single value returned satisfies INTEGERP.

function DEFAULT-EL-VAR-FOR-HL-VAR : (variable)
Return a readable EL var from HL var VARIABLE.
VARIABLE must satisfy VARIABLE-P.

function FULLY-BOUND-P : (object)
Return T iff OBJECT contains no HL variables, and therefore is fully bound.
Single value returned satisfies BOOLEANP.

function VARIABLE-COUNT : ()
Return the total number of HL variables.
Single value returned satisfies INTEGERP.

2.2 KB Indexing

Methods for querying the structures used to index assertions from constants.

function INDEXED-TERM-P : (object)
Returns T iff OBJECT is an indexed CycL term, i.e. a fort or an assertion.
Single value returned satisfies BOOLEANP.

function REMOVE-TERM-INDICES : (term)
Remove all assertions about TERM from the KB. Return the TERM.
Single value returned satisfies INDEXED-TERM-P.

function KEY-EXCEPTION-RULE-INDEX : (rule &optional mt)
Return a list of the keys to the next index level below RULE MT.
Single value returned satisfies LISTP.

function KEY-FUNCTION-RULE-INDEX : (func &optional mt)
Return a list of the keys to the next index level below FUNC MT.
Single value returned satisfies LISTP.

function KEY-GAF-ARG-INDEX : (term &optional argnum pred)
Return a list of the keys to the next index level below TERM ARGNUM PRED.
Single value returned satisfies LISTP.

function KEY-GENL-MT-RULE-INDEX : (col &optional sense mt)
Return a list of the keys to the next index level below COL SENSE MT.
Single value returned satisfies LISTP.

function KEY-GENLS-RULE-INDEX : (col &optional sense mt)
Return a list of the keys to the next index level below COL SENSE MT.
Single value returned satisfies LISTP.

function KEY-ISA-RULE-INDEX : (col &optional sense mt)
Return a list of the keys to the next index level below COL SENSE MT.
Single value returned satisfies LISTP.

function KEY-NART-ARG-INDEX : (term &optional argnum func)
Return a list of the keys to the next index level below TERM ARGNUM FUNC.
Single value returned satisfies LISTP.

function KEY-PREDICATE-EXTENT-INDEX : (pred)
Return a list of the keys to the next predicate-extent index level below PRED.
Single value returned satisfies LISTP.

function KEY-PREDICATE-RULE-INDEX : (pred &optional sense mt)
Return a list of the keys to the next index level below PRED SENSE MT.
Single value returned satisfies LISTP.

function NUM-EXCEPTION-RULE-INDEX : (rule &optional mt direction)
Return the raw assertion count at RULE MT DIRECTION.
Single value returned satisfies INTEGERP.

function NUM-FUNCTION-EXTENT-INDEX : (func)
Return the function extent of FUNC.
Single value returned satisfies INTEGERP.

function NUM-FUNCTION-RULE-INDEX : (func &optional mt direction)
Return the raw assertion count at FUNC MT DIRECTION.
Single value returned satisfies INTEGERP.

function NUM-GAF-ARG-INDEX : (term &optional argnum pred mt)
Return the number of gafs indexed off of TERM ARGNUM PRED MT.
Single value returned satisfies INTEGERP.

function NUM-GENL-MT-RULE-INDEX : (col &optional sense mt direction)
Return the raw assertion count at COL SENSE MT DIRECTION.
Single value returned satisfies INTEGERP.

function NUM-GENLS-RULE-INDEX : (col &optional sense mt direction)
Return the raw assertion count at COL SENSE MT DIRECTION.
Single value returned satisfies INTEGERP.

function NUM-INDEX : (term)
The total number of assertions indexed from TERM.
Single value returned satisfies INTEGERP.

function NUM-ISA-RULE-INDEX : (col &optional sense mt direction)
Return the raw assertion count at COL SENSE MT DIRECTION.
Single value returned satisfies INTEGERP.

function NUM-MT-INDEX : (term)
Return the number of assertions at the mt index for TERM.
Single value returned satisfies INTEGERP.

function NUM-NART-ARG-INDEX : (term &optional argnum func)
Return the number of #$termOfUnit gafs indexed off of TERM ARGNUM FUNC.
Single value returned satisfies INTEGERP.

function NUM-OTHER-INDEX : (term)
Return the number of assertions at the other index for TERM.
Single value returned satisfies INTEGERP.

function NUM-PREDICATE-EXTENT-INDEX : (pred &optional mt)
Return the assertion count at PRED MT.
Single value returned satisfies INTEGERP.

function NUM-PREDICATE-RULE-INDEX : (pred &optional sense mt direction)
Return the raw assertion count at PRED SENSE MT DIRECTION.
Single value returned satisfies INTEGERP.

function RELEVANT-NUM-FUNCTION-EXTENT-INDEX : (func)
Compute the function extent at relevant mts under FUNC.
This will be the entire function extent if #$BaseKB is relevant,
and zero otherwise.
Single value returned satisfies INTEGERP.

function RELEVANT-NUM-GAF-ARG-INDEX : (term &optional argnum pred)
Return the assertion count at relevant mts under TERM ARGNUM PRED.
Single value returned satisfies INTEGERP.

function RELEVANT-NUM-NART-ARG-INDEX : (term &optional argnum func)
Compute the assertion count at relevant mts under TERM ARGNUM FUNC.
This will be the entire count extent if #$BaseKB is relevant,
and zero otherwise.
Single value returned satisfies INTEGERP.

function RELEVANT-NUM-PREDICATE-EXTENT-INDEX : (pred)
Compute the assertion count at relevant mts under PRED.
Single value returned satisfies INTEGERP.

2.3 KB Mapping

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.

2.4 KB Accessors

Miscellaneous methods useful for interacting with the KB

function REFLEXIVE-PREDICATE? : (predicate &optional mt)
Return T iff PREDICATE is a reflexive predicate.
Single value returned satisfies BOOLEANP.

function IRREFLEXIVE-PREDICATE? : (predicate &optional mt)
Return T iff PREDICATE is an irreflexive predicate.
Single value returned satisfies BOOLEANP.

function SYMMETRIC-PREDICATE? : (predicate &optional mt)
Return T iff PREDICATE is a symmetric predicate.
Single value returned satisfies BOOLEANP.

function ASYMMETRIC-PREDICATE? : (predicate &optional mt)
Return T iff PREDICATE is an asymmetric predicate.
Single value returned satisfies BOOLEANP.

function ANTI-SYMMETRIC-PREDICATE? : (predicate &optional mt)
Return T iff PREDICATE is an anti-symmetric predicate.
Single value returned satisfies BOOLEANP.

function TRANSITIVE-PREDICATE? : (predicate &optional mt)
Return T iff PREDICATE is a transitive predicate.
Single value returned satisfies BOOLEANP.

function RELATION? : (relation &optional mt)
Return T iff RELATION is a relationship.
Single value returned satisfies BOOLEANP.

function COMMUTATIVE-RELATION? : (relation &optional mt)
Return T iff RELATION is a commutative relation.
Single value returned satisfies BOOLEANP.

function COMMUTATIVE-FUNCTION? : (function &optional mt)
Return T iff FUNCTION is a commutative function.
Single value returned satisfies BOOLEANP.

function BINARY-PREDICATE? : (predicate &optional mt)
Return T iff PREDICATE is a predicate of arity 2.
Single value returned satisfies BOOLEANP.

function ARGN-ISA : (relation argnum &optional mt)
Returns a list of the local isa constraints applied to the ARGNUMth argument of
RELATION (#$argsIsa conjoins with #$arg1Isa et al).
ARGNUM must satisfy INTEGERP.

function MIN-ARGN-ISA : (relation n &optional mt)
Returns a list of the most specific local isa-constraints applicable
to argument N of RELATION.
RELATION must satisfy INDEXED-TERM-P.
N must satisfy INTEGERP.
Single value returned is a list of elements satisfying INDEXED-TERM-P.

function ARGN-ISA-OF : (collection argnum &optional mt)
Returns the relations for which COLLECTION is a
local isa constraint applied to argument ARGNUM.
ARGNUM must satisfy INTEGERP.
Single value returned is a list of elements satisfying INDEXED-TERM-P.

function ARGN-GENL : (relation argnum &optional mt)
Returns the local genl constraints applied to the ARGNUMth argument of RELATION.
ARGNUM must satisfy INTEGERP.
Single value returned is a list of elements satisfying INDEXED-TERM-P.

function MIN-ARGN-GENL : (relation n &optional mt)
Return a list of the most specific local genl constraints applicable
to the argument N of RELATION.
N must satisfy INTEGERP.
Single value returned is a list of elements satisfying FORT-P.

function ARGN-GENL-OF : (collection argnum &optional mt)
Returns a list of the predicates for which COLLECTION is a
local genl constraint applied to the Nth argument.
ARGNUM must satisfy INTEGERP.
Single value returned is a list of elements satisfying FORT-P.

function DEFINING-DEFNS : (col &optional mt)
Return a list of the local defining (necessary and sufficient definitions) of collection COL.
Single value returned is a list of elements satisfying FORT-P.

function NECESSARY-DEFNS : (col &optional mt)
Return a list of the local necessary definitions of collection COL.
Single value returned is a list of elements satisfying FORT-P.

function SUFFICIENT-DEFNS : (col &optional mt)
Return a list of the local sufficient definitions of collection COL.
Single value returned is a list of elements satisfying FORT-P.

function ALL-SUFFICIENT-DEFNS : (col &optional mt)
Return a list of all sufficient definitions of collection COL.
Single value returned is a list of elements satisfying FORT-P.

function ARITY : (relation &optional mt)
Return the arity for relation constant RELATION.

function RESULT-ISA : (functor &optional mt)
Return a list of the collections that include as instances
the results of non-predicate function constant FUNCTOR.
Single value returned is a list of elements satisfying FORT-P.

function CREATOR : (fort &optional mt)
Identify the cyclist who created FORT.
FORT must satisfy FORT-P.
MT must satisfy HLMT-P.
Single value returned satisfies FORT-P.

function CREATION-TIME : (fort &optional mt)
Identify when FORT was created.
FORT must satisfy FORT-P.
MT must satisfy HLMT-P.
Single value returned satisfies INTEGERP.

function COMMENT : (fort &optional mt)
Return the comment string for FORT.
FORT must satisfy FORT-P.
Single value returned satisfies STRINGP.

function ASSERTED-BY : (assertion)
Returns the cyclist who asserted ASSERTION.
ASSERTION must satisfy ASSERTION-P.

function ASSERTED-WHEN : (assertion)
Returns the date when ASSERTION was asserted.
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies INTEGERP.

function REVIEWER : (fort &optional mt)
Identify the cyclist who reviewed FORT.
FORT must satisfy FORT-P.
MT must satisfy HLMT-P.
Single value returned satisfies FORT-P.

function ALL-TERM-ASSERTIONS : (term &optional remove-duplicates?)
Return a list of all the assertions indexed via the indexed term TERM.
TERM must satisfy INDEXED-TERM-P.
Single value returned is a list of elements satisfying ASSERTION-P.

function ISA-RELEVANT-ASSERTIONS : (term &optional mt)
Return a list of all (e.g., inheritance) rules relevant to TERM
by virtue of the collections of which it is an instance.
Single value returned is a list of elements satisfying ASSERTION-P.

function ASSERTIONS-MENTIONING-TERMS : (term-list &optional include-meta-assertions?)
Return a list of assertions that mention every term in TERM-LIST.
Single value returned is a list of elements satisfying ASSERTION-P.

function PRIMITIVE-COLLECTION? : (fort &optional mt)
Return T iff FORT is a collection for which no classical (necessary and sufficient)
definition is known.
Single value returned satisfies BOOLEANP.

function PREDS-FOR-PAIR : (fort-1 fort-2 &optional mt mode)
Return a list of the predicates relevant to relating FORT-1 and FORT-2.
MODE may be :figurative (instances of collections),
:literal (constants), or
:mixed (referents).
FORT-1 must satisfy FORT-P.
FORT-2 must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function COLLECTIONS-COEXTENSIONAL? : (col-1 col-2 &optional mt)
Are COL-1 and COL-2 coextensional?
COL-1 must satisfy EL-FORT-P.
COL-2 must satisfy EL-FORT-P.
Single value returned satisfies BOOLEANP.

function COLLECTIONS-DISJOINT? : (col-1 col-2 &optional mt)
Are collections COL-1 and COL-2 disjoint?
(uses only sbhl graphs: their extensions are not searched
nor are their necessary conditions analyzed)
COL-1 must satisfy EL-FORT-P.
COL-2 must satisfy EL-FORT-P.
Single value returned satisfies BOOLEANP.

function COLLECTIONS-INTERSECT? : (col-1 col-2 &optional mt)
Do collections COL-1 and COL-2 intersect?
(uses only sbhl graphs: their extensions are not searched
nor are their sufficient conditions analyzed)
COL-1 must satisfy EL-FORT-P.
COL-2 must satisfy EL-FORT-P.
Single value returned satisfies BOOLEANP.

function COUNT-ALL-INSTANCES : (collection &optional mt tv)
Counts the number of instances in the collection and then returns the count.
COLLECTION must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

2.5 Epistemological-Level Support

Methods that support the EL

function EL-STRENGTH-P : (object)
Return T iff OBJECT is a valid CycL assertion strength
:default or :monotonic.
Single value returned satisfies BOOLEANP.

function EL-TO-HL : (formula &optional mt)
Translate el expression FORMULA into its equivalent canonical hl expressions
FORMULA must satisfy EL-FORMULA-P.

function EL-TO-HL-QUERY : (formula &optional mt)
Translate el query FORMULA into its equivalent hl expressions
FORMULA must satisfy EL-FORMULA-P.

function ASSERTION-EL-FORMULA : (assertion)
Return the el formula for ASSERTION
ASSERTION must satisfy ASSERTION-P.
Single value returned satisfies LISTP.

function EL-WFF-SYNTAX? : (formula &optional mt)
Is FORMULA well-formed wrt syntax?
Single value returned satisfies BOOLEANP.

function EL-WFF-SYNTAX+ARITY? : (formula &optional mt)
Is FORMULA well-formed wrt syntax and arity?
Single value returned satisfies BOOLEANP.

function GROUND? : (expression &optional var?)
Returns whether EXPRESSION is free of any variables?
Single value returned satisfies BOOLEANP.

function EL-FORMULA-OK? : (formula &optional mt)
Is FORMULA a well-formed el formula?
FORMULA must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function EL-QUERY-OK? : (formula &optional mt)
Is FORMULA a well-formed el query?
FORMULA must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function DIAGNOSE-EL-FORMULA : (formula &optional mt io-mode)
Identify how el formula FORMULA fails syntactic or semantic constraints
FORMULA must satisfy LISTP.

2.6 Transitivity HL Modules

Methods that support general transitivity reasoning using transitive relations.

2.6.1 Subsumption-Based HL Modules

Methods that provide support efficient transitivity reasoning over the sbhl relations.

2.6.1.1 #$isa support

function MIN-ISA : (term &optional mt tv)
Returns most-specific collections that include TERM (inexpensive)
TERM must satisfy HL-TERM-P.
Single value returned is a list of elements satisfying FORT-P.

function MAX-NOT-ISA : (term &optional mt tv)
Returns most-general collections that do not include TERM (expensive)
TERM must satisfy HL-TERM-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-ISA : (term &optional mt tv)
Returns all collections that include TERM (inexpensive)
TERM must satisfy HL-TERM-P.
Single value returned is a list of elements satisfying FORT-P.

function UNION-ALL-ISA : (terms &optional mt tv)
Returns all collections that include any term in TERMS (inexpensive)
TERMS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function ALL-NOT-ISA : (term &optional mt tv)
Returns all collections that do not include TERM (expensive)
TERM must satisfy HL-TERM-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-INSTANCES : (col &optional mt tv)
Returns all instances of COLLECTION (expensive)
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MAP-ALL-ISA : (fn term &optional mt tv)
Apply FUNCTION to every all-isa of TERM
(FUNCTION must not effect the current sbhl search state)
FN must satisfy FUNCTION-SPEC-P.
TERM must satisfy HL-TERM-P.

function ANY-WRT-ALL-ISA : (function term &optional mt tv)
Return the first encountered non-nil result of applying FUNCTION to the all-isa of TERM
(FUNCTION may not effect the current sbhl search state)
FUNCTION must satisfy FUNCTION-SPEC-P.
TERM must satisfy HL-TERM-P.

function MAP-ALL-INSTANCES : (fn col &optional mt tv)
Apply FUNCTION to each unique instance of all specs of COLLECTION.
FN must satisfy FUNCTION-SPEC-P.
COL must satisfy EL-FORT-P.

function MAP-INSTANCES : (function term &optional mt tv)
apply FUNCTION to every (least general) #$isa of TERM
FUNCTION must satisfy FUNCTION-SPEC-P.
TERM must satisfy EL-FORT-P.

function ISA? : (term collection &optional mt tv)
Returns whether TERM is an instance of COLLECTION
COLLECTION must satisfy EL-FORT-P.
Single value returned satisfies BOOLEANP.

function ISA-ANY? : (term collections &optional mt tv)
Returns whether TERM is an instance of any collection in COLLECTIONS
TERM must satisfy HL-TERM-P.
COLLECTIONS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function ANY-ISA-ANY? : (terms collections &optional mt tv)
@return booleanp; whether any term in TERMS is an instance of any collection in COLLECTIONS
TERMS must satisfy LISTP.
COLLECTIONS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function NOT-ISA? : (term collection &optional mt tv)
@return boolenap; whether TERM is known to not be an instance of COLLECTION
TERM must satisfy HL-TERM-P.
COLLECTION must satisfy EL-FORT-P.
Single value returned satisfies BOOLEANP.

function INSTANCES? : (collection &optional mt tv)
Returns whether COLLECTION has any direct instances
COLLECTION must satisfy EL-FORT-P.
Single value returned satisfies BOOLEANP.

function INSTANCES : (col &optional mt tv)
Returns the asserted instances of COL
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ISA-SIBLINGS : (term &optional mt tv)
Returns the direct isas of those collections of which TERM is a direct instance
TERM must satisfy HL-TERM-P.
Single value returned is a list of elements satisfying FORT-P.

function MAX-FLOOR-MTS-OF-ISA-PATHS : (term collection &optional tv)
Returns in what (most-genl) mts TERM is an instance of COLLECTION
TERM must satisfy HL-TERM-P.
COLLECTION must satisfy EL-FORT-P.

function WHY-ISA? : (term collection &optional mt tv behavior)
Returns justification of (isa TERM COLLECTION)
TERM must satisfy HL-TERM-P.
COLLECTION must satisfy EL-FORT-P.
Single value returned satisfies LISTP.

function WHY-NOT-ISA? : (term collection &optional mt tv behavior)
Returns justification of (not (isa TERM COLLECTION))
TERM must satisfy HL-TERM-P.
COLLECTION must satisfy EL-FORT-P.
Single value returned satisfies LISTP.

function ALL-INSTANCES-AMONG : (col terms &optional mt tv)
Returns those elements of TERMS that include COL as an all-isa
COL must satisfy HL-TERM-P.
TERMS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function ALL-ISA-AMONG : (term collections &optional mt tv)
Returns those elements of COLLECTIONS that include TERM as an all-instance
TERM must satisfy HL-TERM-P.
COLLECTIONS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function ALL-ISAS-WRT : (term isa &optional mt tv)
Returns all isa of term TERM that are also instances of collection ISA (ascending transitive closure; inexpensive)
TERM must satisfy EL-FORT-P.
ISA must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function INSTANCE-SIBLINGS : (term &optional mt tv)
Returns the direct instances of those collections having direct isa TERM
TERM must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MAX-INSTANCES : (col &optional mt tv)
Returns the maximal among the asserted instances of COL
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MIN-NOT-INSTANCES : (col &optional mt tv)
Returns the most-specific negated instances of collection COL
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function NOT-ISA-AMONG : (term collections &optional mt tv)
Returns those elements of COLLECTIONS that do NOT include TERM
TERM must satisfy HL-TERM-P.
COLLECTIONS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function UNION-ALL-INSTANCES : (cols &optional mt tv)
Returns set of all instances of each collection in COLS (expensive)
COLS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

2.6.1.2 #$genls support

function MIN-GENLS : (col &optional mt tv)
Returns the most-specific genls of collection COL
Single value returned is a list of elements satisfying FORT-P.

function MAX-NOT-GENLS : (col &optional mt tv)
Returns the least-specific negated genls of collection COL
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MAX-SPECS : (col &optional mt tv)
Returns the least-specific specs of collection COL
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MIN-NOT-SPECS : (col &optional mt tv)
Returns the most-specific negated specs of collection COL
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GENL-SIBLINGS : (col &optional mt tv)
Returns the direct genls of those direct spec collections of COL
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function SPEC-SIBLINGS : (col &optional mt tv)
Returns the direct specs of those direct genls collections of COL
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-GENLS : (col &optional mt tv)
Returns all genls of collection COL
(ascending transitive closure; inexpensive)
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-GENLS-WRT : (spec genl &optional mt tv)
Returns all genls of collection SPEC that are also specs of collection GENL (ascending transitive closure; inexpensive)
SPEC must satisfy EL-FORT-P.
GENL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function UNION-ALL-GENLS : (cols &optional mt tv)
Returns all genls of each collection in COLs
COLS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function ALL-GENLS-IF : (function col &optional mt tv)
Returns all genls of collection COL that satisfy FUNCTION
(FUNCTION must not effect sbhl search state)
FUNCTION must satisfy FUNCTION-SPEC-P.
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-NOT-GENLS : (col &optional mt tv)
Returns all negated genls of collection COL
(descending transitive closure; expensive)
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-SPECS : (col &optional mt tv)
Returns all specs of collection COL
(descending transitive closure; expensive)
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-SPECS-IF : (function col &optional mt tv)
Returns all genls of collection COL that satisfy FUNCTION
(FUNCTION must not effect sbhl search state)
FUNCTION must satisfy FUNCTION-SPEC-P.
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-DEPENDENT-SPECS : (col &optional mt tv)
Returns all specs s of COL s.t. every path connecting
s to any genl of COL must pass through COL
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function UNION-ALL-SPECS : (cols &optional mt tv)
Returns all specs of each collection in COLs
COLS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function GENL? : (spec genl &optional mt tv)
Returns whether (#$genls SPEC GENL) can be inferred.
(ascending transitive search; inexpensive)
SPEC must satisfy EL-FORT-P.
GENL must satisfy EL-FORT-P.
Single value returned satisfies BOOLEANP.

function SPEC? : (genl spec &optional mt tv)
Returns whether (#$genls SPEC GENL) can be inferred.
(ascending transitive search; inexpensive)
GENL must satisfy EL-FORT-P.
SPEC must satisfy EL-FORT-P.
Single value returned satisfies BOOLEANP.

function ANY-GENL? : (spec genls &optional mt tv)
(any-genl? spec genls) is t iff (genl? spec genl) for some genl in genls
(ascending transitive search; inexpensive)
SPEC must satisfy EL-FORT-P.
GENLS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function ALL-GENL? : (spec genls &optional mt tv)
Returns T iff (genl? spec genl) for every genl in GENLS
(ascending transitive search; inexpensive)
SPEC must satisfy EL-FORT-P.
GENLS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function ANY-SPEC? : (genl specs &optional mt tv)
Returns T iff (spec? genl spec) for some spec in SPECS
GENL must satisfy EL-FORT-P.
SPECS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function ALL-SPEC? : (genl specs &optional mt tv)
Returns T iff (spec? genl spec) for every spec in SPECS
GENL must satisfy EL-FORT-P.
SPECS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function ANY-GENL-ANY? : (specs genls &optional mt tv)
Return T iff (genl? spec genl mt) for any spec in SPECS, genl in GENLS
SPECS must satisfy LISTP.
GENLS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function ANY-GENL-ALL? : (specs genls &optional mt tv)
Return T iff (genl? spec genl mt) for any spec in SPECS and all genl in GENLS
SPECS must satisfy LISTP.
GENLS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function NOT-GENL? : (col not-genl &optional mt tv)
Return whether collection NOT-GENL is not a genl of COL.
COL must satisfy EL-FORT-P.
NOT-GENL must satisfy EL-FORT-P.
Single value returned satisfies BOOLEANP.

function ANY-NOT-GENL? : (col not-genls &optional mt tv)
Returns whether any collection in NOT-GENLS is not a genl of COL.
COL must satisfy EL-FORT-P.
NOT-GENLS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function COLLECTION-LEAVES : (col &optional mt tv)
Returns the minimally-general (the most specific) among all-specs of COL
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MIN-COLS : (cols &optional mt tv)
Returns the minimally-general (the most specific) among reified collections COLS
COLS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function MAX-COLS : (cols &optional mt tv)
Returns the most-general among reified collections COLS
COLS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function MIN-CEILING-COLS : (cols &optional candidates mt tv)
Returns the most specific common generalizations among reified collections COLS
(if CANDIDATES is non-nil, then result is a subset of CANDIDATES)
COLS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function MAX-FLOOR-COLS : (cols &optional candidates mt tv)
Returns the most general common specializations among reified collections COLS
(if CANDIDATES is non-nil, then result is a subset of CANDIDATES)
COLS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function ANY-DISJOINT-COLLECTION-PAIR : (cols &optional mt)
Returns a pair of disjoint elements of COLS (if any exist)
COLS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function ANY-DISJOINT-COLLECTION-PAIR? : (cols &optional mt)
Are any two collections in COLS disjoint?
COLS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function WHY-COLLECTIONS-DISJOINT? : (c1 c2 &optional mt)
Justification of (disjointWith C1 C2)
C1 must satisfy EL-FORT-P.
C2 must satisfy EL-FORT-P.
Single value returned satisfies LISTP.

function ANY-GENL-ISA : (col isa &optional mt tv)
Return some genl of COL that isa instance of ISA (if any such genl exists)
COL must satisfy EL-FORT-P.
ISA must satisfy EL-FORT-P.
Single value returned satisfies FORT-P.

function LIGHTER-COL : (col-a col-b)
Return COL-B iff it has fewer specs than COL-A, else return COL-A
COL-A must satisfy EL-FORT-P.
COL-B must satisfy EL-FORT-P.
Single value returned satisfies FORT-P.

function SHALLOWER-COL : (col-a col-b)
Return COL-B iff it has fewer genls than COL-A, else return COL-A
COL-A must satisfy EL-FORT-P.
COL-B must satisfy EL-FORT-P.
Single value returned satisfies FORT-P.

function MAX-FLOOR-MTS-OF-GENLS-PATHS : (spec genl &optional tv)
@return listp; Returns in what (most-genl) mts GENL is a genls of SPEC
SPEC must satisfy EL-FORT-P.
GENL must satisfy EL-FORT-P.

function WHY-NOT-ASSERT-GENLS? : (spec genl &optional mt)
Justification of why asserting (genls SPEC GENL) is not consistent
SPEC must satisfy EL-FORT-P.
GENL must satisfy EL-FORT-P.
Single value returned satisfies LISTP.

function MAP-ALL-GENLS : (fn col &optional mt tv)
Applies FN to every (all) genls of COL
(FN must not effect the current sbhl space)
FN must satisfy FUNCTION-SPEC-P.
COL must satisfy EL-FORT-P.

function ANY-ALL-GENLS : (fn col &optional mt tv)
Return a non-nil result of applying FN to some all-genl of COL
(FN must not effect the current sbhl space)
FN must satisfy FUNCTION-SPEC-P.
COL must satisfy EL-FORT-P.

function MAP-ALL-SPECS : (fn col &optional mt tv)
Applies FN to every (all) specs of COL
(FN must not effect the current sbhl space)
FN must satisfy FUNCTION-SPEC-P.
COL must satisfy EL-FORT-P.

function ANY-ALL-SPECS : (fn col &optional mt tv)
Return a non-nil result of applying FN to some all-spec of COL
(FN must not effect the current sbhl space)
FN must satisfy FUNCTION-SPEC-P.
COL must satisfy EL-FORT-P.

function ALL-GENLS-AMONG : (col candidates &optional mt tv)
Returns those genls of COL that are included among CANDIDATEs
COL must satisfy EL-FORT-P.
CANDIDATES must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function ALL-NOT-SPEC? : (col not-specs &optional mt tv)
Return whether every collection in NOT-SPECS is not a spec of COL.
COL must satisfy EL-FORT-P.
NOT-SPECS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function ALL-NOT-SPECS : (col &optional mt tv)
Returns all negated specs of collection COL
(ascending transitive closure; inexpensive)
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-SPEC-ANY? : (specs genls &optional mt tv)
Return T iff for each spec in SPECS there is some genl in GENLS s.t. (genl? spec genl mt)
SPECS must satisfy LISTP.
GENLS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function ALL-SPECS-AMONG : (col candidates &optional mt tv)
Returns those specs of COL that are included among CANDIDATEs
COL must satisfy EL-FORT-P.
CANDIDATES must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function SPEC-SIBLINGS : (col &optional mt tv)
Returns the direct specs of those direct genls collections of COL
COL must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function WHY-GENL? : (spec genl &optional mt tv behavior)
Justification of (genls SPEC GENL)
SPEC must satisfy EL-FORT-P.
GENL must satisfy EL-FORT-P.
Single value returned satisfies LISTP.

function WHY-NOT-GENL? : (spec genl &optional mt tv behavior)
Justification of (not (genls SPEC GENL))
SPEC must satisfy EL-FORT-P.
GENL must satisfy EL-FORT-P.
Single value returned satisfies LISTP.

2.6.1.3 #$genlPreds and #$genlInverse support

function MIN-GENL-PREDICATES : (pred &optional mt tv)
Returns the most-specific local genlPreds of PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MIN-GENL-INVERSES : (pred &optional mt tv)
Returns the most-specific local genlInverses of PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MAX-NOT-GENL-PREDICATES : (pred &optional mt tv)
Returns the most-general local negated genlPreds of PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MAX-NOT-GENL-INVERSES : (pred &optional mt tv)
Returns the most-general local negated genlPreds of PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MAX-SPEC-PREDICATES : (pred &optional mt tv)
Returns the most-general specPreds of PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MAX-SPEC-INVERSES : (pred &optional mt tv)
Returns the most-general specInverses of PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MIN-NOT-SPEC-PREDICATES : (pred &optional mt tv)
Returns the most-specific negated specPreds of PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function MIN-NOT-SPEC-INVERSES : (pred &optional mt tv)
Returns the most-specific negated specPreds of PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GENL-PREDICATE-SIBLINGS : (pred &optional mt tv)
Returns the direct #$genlPreds of those predicates having direct spec-preds PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GENL-INVERSE-SIBLINGS : (pred &optional mt tv)
Returns the direct #$genlInverse of those predicates having direct spec-inverses PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function SPEC-PREDICATE-SIBLINGS : (pred &optional mt tv)
Returns the direct spec-preds of those collections having direct #$genlPreds PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function SPEC-INVERSE-SIBLINGS : (pred &optional mt tv)
Returns the direct spec-inverses of those collections having direct #$genlInverse PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-GENL-PREDICATES : (pred &optional mt tv)
Returns all genlPreds of predicate PRED
(ascending transitive closure; inexpensive)
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-GENL-INVERSES : (pred &optional mt tv)
Returns all genlPreds of predicate PRED
(ascending transitive closure; inexpensive)
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-NOT-GENL-PREDICATES : (pred &optional mt tv)
Returns all negated genlPreds of predicate PRED
(descending transitive closure; expensive)
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-NOT-GENL-INVERSES : (pred &optional mt tv)
Returns all negated genlPreds of predicate PRED
(descending transitive closure; expensive)
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-SPEC-PREDICATES : (pred &optional mt tv)
Returns all predicates having PRED as a genlPred
(descending transitive closure; expensive)
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-SPEC-INVERSES : (pred &optional mt tv)
Returns all predicates having PRED as a genlInverse
(descending transitive closure; expensive)
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-SPEC-PREDS-WRT-TYPE : (pred col arg &optional mt tv)
Returns those all-spec-preds of PRED for which instances
of COL are legal in arguments in position ARG
PRED must satisfy FORT-P.
COL must satisfy FORT-P.
ARG must satisfy INTEGERP.
Single value returned is a list of elements satisfying FORT-P.

function ALL-SPEC-PREDS-WRT-ARG : (pred fort arg &optional mt tv)
Returns those all-spec-preds of PRED for which FORT
is legal as arguments in position ARG
PRED must satisfy FORT-P.
FORT must satisfy FORT-P.
ARG must satisfy INTEGERP.
Single value returned is a list of elements satisfying FORT-P.

function ALL-NOT-SPEC-PREDICATES : (pred &optional mt tv)
Returns all negated specPreds of predicate PRED
(ascending transitive closure; inexpensive)
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-NOT-SPEC-INVERSES : (pred &optional mt tv)
Returns all predicates having PRED as a negated genlInverse
(ascending transitive closure; inexpensive)
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function SPEC-PREDICATE? : (genl spec &optional mt tv)
Is GENL a genlPred of SPEC?
(ascending transitive search; inexpensive)
GENL must satisfy FORT-P.
SPEC must satisfy FORT-P.
Single value returned satisfies BOOLEANP.

function GENL-PREDICATE? : (spec genl &optional mt tv)
Is GENL a genlPred of SPEC?
(ascending transitive search; inexpensive)
SPEC must satisfy FORT-P.
GENL must satisfy FORT-P.
Single value returned satisfies BOOLEANP.

function GENL-INVERSE? : (spec genl &optional mt tv)
Is GENL a genlInverse of SPEC?
(ascending transitive search; inexpensive)
SPEC must satisfy FORT-P.
GENL must satisfy FORT-P.
Single value returned satisfies BOOLEANP.

function SPEC-INVERSE? : (genl spec &optional mt tv)
Is GENL a genlInverse of SPEC?
(ascending transitive search; inexpensive)
SPEC must satisfy FORT-P.
GENL must satisfy FORT-P.
Single value returned satisfies BOOLEANP.

function ANY-GENL-PREDICATE? : (spec genls &optional mt tv)
Returns T iff (genl-predicate? SPEC GENL) for some genl in GENLS
(ascending transitive search; inexpensive)
SPEC must satisfy FORT-P.
GENLS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function NOT-GENL-PREDICATE? : (spec not-genl &optional mt tv)
Is NOT-GENL knwon to be not a genlPred of SPEC?
(descending transitive search; expensive)
SPEC must satisfy FORT-P.
NOT-GENL must satisfy FORT-P.
Single value returned satisfies BOOLEANP.

function NOT-GENL-INVERSE? : (spec not-genl &optional mt tv)
Is NOT-GENL a negated genlInverse of SPEC?
(descending transitive search; expensive)
SPEC must satisfy FORT-P.
NOT-GENL must satisfy FORT-P.
Single value returned satisfies BOOLEANP.

function ANY-NOT-GENL-PREDICATE? : (pred not-genls &optional mt tv)
Is any predicate in NOT-GENLS not a genlPred of PRED?
(desc