Formalized Common Knowledge

Projects

FAQ

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.

	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?
(descending transitive search; expensive)
PRED must satisfy FORT-P.
NOT-GENLS must satisfy LISTP.
Single value returned satisfies BOOLEANP.

function INTERSECTING-PREDICATES? : (pred1 pred2 &optional mt)
Does the extension of PRED1 include some tuple in the extension of PRED2?
PRED1 must satisfy FORT-P.
PRED2 must satisfy FORT-P.
Single value returned satisfies BOOLEANP.

function WHY-GENL-PREDICATE? : (spec genl &optional mt tv behavior)
A justification of (genlPreds SPEC GENL)
SPEC must satisfy FORT-P.
GENL must satisfy FORT-P.
Single value returned satisfies LISTP.

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

function WHY-GENL-INVERSE? : (pred genl-inverse &optional mt tv behavior)
A justification of (genlInverse PRED GENL-INVERSE)
PRED must satisfy FORT-P.
GENL-INVERSE must satisfy FORT-P.
Single value returned satisfies LISTP.

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

function MIN-PREDICATES : (preds &optional mt tv)
Returns the most-specific predicates in PREDS
PREDS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function MAX-PREDICATES : (preds &optional mt tv)
Returns the most-specific predicates in PREDS
PREDS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function MIN-CEILING-PREDICATES : (preds &optional candidates mt tv)
Returns the most-specific common generalizations (ceilings) of PREDS
PREDS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function MAX-FLOOR-PREDICATES : (preds &optional candidates mt tv)
Returns the most-general common specializations (floors) of PREDS
PREDS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function MAX-FLOOR-MTS-OF-GENL-PREDICATE-PATHS : (spec genl &optional tv)
@return listp; In what (most-genl) mts is GENL a genlPred of SPEC?
SPEC must satisfy FORT-P.
GENL must satisfy FORT-P.

function MAX-FLOOR-MTS-OF-GENL-INVERSE-PATHS : (spec genl-inverse &optional tv)
In what (most-genl) mts is GENL-INVERSE a genlInverse of SPEC?
SPEC must satisfy FORT-P.
GENL-INVERSE must satisfy FORT-P.

function MAP-ALL-GENL-PREDS : (pred fn &optional mt tv)
Apply FN to each genlPred of PRED
PRED must satisfy FORT-P.
FN must satisfy FUNCTION-SPEC-P.

function SOME-ALL-GENL-PREDS : (pred fn &optional mt tv)
Apply FN to each genlPred of PRED until FN returns a non-nil result
PRED must satisfy FORT-P.
FN must satisfy FUNCTION-SPEC-P.

function MAP-ALL-SPEC-PREDS : (pred fn &optional mt tv)
Apply FN to each genlPred of PRED
PRED must satisfy FORT-P.
FN must satisfy FUNCTION-SPEC-P.

function SOME-ALL-SPEC-PREDS : (pred fn &optional mt tv)
Apply FN to each genlPred of PRED until FN returns a non-nil result
PRED must satisfy FORT-P.
FN must satisfy FUNCTION-SPEC-P.

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

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

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

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

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

function 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 NOT-SPEC-PREDICATES : (pred &optional mt tv)
Returns the negated specPreds of PRED
PRED must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function SOME-ALL-GENL-INVERSES : (pred fn &optional mt tv)
Apply FN to each genlPred of PRED until FN returns a non-nil result
PRED must satisfy FORT-P.
FN must satisfy FUNCTION-SPEC-P.

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

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

function UNION-ALL-GENL-INVERSES : (preds &optional mt tv)
Returns all genl-inverses of each collection in Preds
PREDS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function UNION-ALL-GENL-PREDICATES : (preds &optional mt tv)
Returns all genl-predicates of each collection in Preds
PREDS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function UNION-ALL-SPEC-INVERSES : (preds &optional mt tv)
Returns all specs of each collection in Preds
PREDS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function UNION-ALL-SPEC-PREDICATES : (preds &optional mt tv)
Returns all spec-predicates of each collection in Preds
PREDS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

2.6.1.4 General transitivity support

function GT-ALL-ACCESSIBLE : (predicate fort &optional mt)
Returns all superiors and all inferiors of FORT via PREDICATE
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-ALL-DEPENDENT-INFERIORS : (predicate fort &optional mt)
Returns all inferiors i of FORT s.t. every path connecting i to
any superior of FORT must pass through FORT
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-ALL-INFERIORS : (predicate fort &optional mt)
Returns all inferiors of FORT via PREDICATE
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-ALL-SUPERIORS : (predicate fort &optional mt)
Returns all superiors of FORT via PREDICATE
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-ANY-SUPERIOR-PATH : (predicate inferior superior &optional mt)
Returns list of nodes connecting INFERIOR with SUPERIOR
PREDICATE must satisfy FORT-P.
INFERIOR must satisfy FORT-P.
SUPERIOR must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-CO-INFERIORS : (predicate fort &optional mt)
Returns sibling direct-inferiors of direct-superiors of FORT via PREDICATE, excluding FORT itself
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-CO-SUPERIORS : (predicate fort &optional mt)
Returns sibling direct-superiors of direct-inferiors of FORT via PREDICATE, excluding FORT itself
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-COMPLETES-CYCLE? : (predicate fort1 fort2 &optional mt)
Returns whether a transitive path connect FORT2 to FORT1,
or whether a transitive inverse path connect FORT1 to FORT2?
PREDICATE must satisfy FORT-P.
FORT1 must satisfy FORT-P.
FORT2 must satisfy FORT-P.
Single value returned satisfies BOOLEANP.

function GT-COMPOSE-FN-ALL-INFERIORS : (predicate fort fn &optional combine-fn mt)
Apply fn to each inferior of FORT;
fn takes a fort as its only arg, and
it must not effect the search status of each fort it visits
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
FN must satisfy FUNCTION-SPEC-P.

function GT-COMPOSE-FN-ALL-SUPERIORS : (predicate fort fn &optional combine-fn mt)
Apply fn to each superior of FORT;
fn takes a fort as its only arg, and must not effect the search status of each
fort it visits
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
FN must satisfy FUNCTION-SPEC-P.

function GT-COMPOSE-PRED-ALL-INFERIORS : (predicate fort compose-pred &optional compose-index-arg compose-gather-arg mt)
Returns all nodes accessible by COMPOSE-PRED from each inferior of FORT along
transitive PREDICATE
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
COMPOSE-PRED must satisfy PREDICATE-IN-ANY-MT?.
Single value returned is a list of elements satisfying FORT-P.

function GT-COMPOSE-PRED-ALL-SUPERIORS : (predicate fort compose-pred &optional compose-index-arg compose-gather-arg mt)
Returns all nodes accessible by COMPOSE-PRED from each superior of FORT along
transitive PREDICATE
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
COMPOSE-PRED must satisfy PREDICATE-IN-ANY-MT?.
Single value returned is a list of elements satisfying FORT-P.

function GT-CYCLES? : (predicate fort &optional mt)
Returns whether FORT is accessible from itself by one or more PREDICATE gafs?
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned satisfies BOOLEANP.

function GT-HAS-INFERIOR? : (predicate superior inferior &optional mt)
Returns whether fort SUPERIOR is hierarchically higher
(wrt transitive PREDICATE) to fort INFERIOR?
PREDICATE must satisfy FORT-P.
SUPERIOR must satisfy FORT-P.
INFERIOR must satisfy FORT-P.
Single value returned satisfies BOOLEANP.

function GT-HAS-SUPERIOR? : (predicate inferior superior &optional mt)
Returns whetherfort INFERIOR is hierarchically lower (wrt transitive PREDICATE)
to fort SUPERIOR?
PREDICATE must satisfy FORT-P.
INFERIOR must satisfy FORT-P.
SUPERIOR must satisfy FORT-P.
Single value returned satisfies BOOLEANP.

function GT-INFERIORS : (predicate fort &optional mt)
Returns direct inferiors of FORT via transitive PREDICATE
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-LEAVES : (predicate fort &optional mt)
Returns minimal inferiors (i.e., leaves) of FORT via PREDICATE
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-MAX-FLOORS : (predicate forts &optional candidates mt)
Returns the least-subordinate elements or common inferiors of FORTS
(when CANDIDATES is non-nil, the result must subset it)
PREDICATE must satisfy FORT-P.
FORTS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function GT-MAX-INFERIORS : (predicate fort &optional mt)
Returns maximal inferiors of FORT via transitive PREDICATE
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-MAX-INFERIORS-EXCLUDING : (predicate inferior superior &optional mt)
Returns most-general inferiors of SUPERIOR ignoring INFERIOR (expensive)
(useful for splicing-out INFERIOR from hierarchy)
PREDICATE must satisfy FORT-P.
INFERIOR must satisfy FORT-P.
SUPERIOR must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-MAX-NODES : (predicate forts &optional mt direction)
Returns returns the least-subordinate elements of FORTS
(<direction> should be :up unless all nodes are low in the hierarchy)
PREDICATE must satisfy FORT-P.
FORTS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function GT-MIN-CEILINGS : (predicate forts &optional candidates mt)
Returns the most-subordinate common superiors of FORTS
(when CANDIDATES is non-nil, the result must subset it)
PREDICATE must satisfy FORT-P.
FORTS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function GT-MIN-NODES : (predicate forts &optional mt)
Returns returns the most-subordinate elements of FORTS
(one member only of a cycle will be a min-node candidate)
PREDICATE must satisfy FORT-P.
FORTS must satisfy LISTP.
Single value returned is a list of elements satisfying FORT-P.

function GT-MIN-SUPERIORS : (predicate fort &optional mt)
Returns minimal superiors of FORT via transitive PREDICATE
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-MIN-SUPERIORS-EXCLUDING : (predicate inferior superior &optional mt)
Returns least-general superiors of INFERIOR ignoring SUPERIOR
(useful for splicing-out SUPERIOR from hierarchy)
PREDICATE must satisfy FORT-P.
INFERIOR must satisfy FORT-P.
SUPERIOR must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-REDUNDANT-INFERIORS : (predicate fort &optional mt)
Returns direct-inferiors of FORT via PREDICATE that subsumed other inferiors
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-REDUNDANT-SUPERIORS : (predicate fort &optional mt)
Returns direct-superiors of FORT via PREDICATE that are subsumed by other superiors
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-ROOTS : (predicate fort &optional mt)
Returns maximal superiors (i.e., roots) of FORT via PREDICATE
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-SUPERIORS : (predicate fort &optional mt)
Returns direct superiors of FORT via transitive PREDICATE
PREDICATE must satisfy FORT-P.
FORT must satisfy FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function GT-WHY-COMPLETES-CYCLE? : (predicate fort1 fort2 &optional mt)
Returns justification that a transitive path connects FORT2 to FORT1,
or that a transitive inverse path connects FORT1 to FORT2?
PREDICATE must satisfy FORT-P.
FORT1 must satisfy FORT-P.
FORT2 must satisfy FORT-P.

function GT-WHY-SUPERIOR? : (predicate superior inferior &optional mt)
Returns justification of why SUPERIOR is superior to (i.e., hierarchically higher than)
INFERIOR
PREDICATE must satisfy FORT-P.
SUPERIOR must satisfy FORT-P.
INFERIOR must satisfy FORT-P.
Single value returned is a list of elements satisfying ASSERTION-P.

2.6.1.5 #$genlAttributes support

function ALL-GENL-ATTRIBUTES : (att &optional mt tv)
Returns all genl-attributes of attribute ATT
(ascending transitive closure; inexpensive)
ATT must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-GENL-ATTRIBUTES-IF : (function att &optional mt tv)
Returns all genl-attributes of attribute ATT that satisfy FUNCTION
(FUNCTION must not effect sbhl search state)
FUNCTION must satisfy FUNCTION-SPEC-P.
ATT must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-GENL-ATTRIBUTES-WRT : (spec genl &optional mt tv)
Returns all genl-attributes of attribute SPEC that are also specs of attribute 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 ARGN-GENL-ATTRIBUTE : (relation n &optional mt)
Returns the local genl-attribute constraints applied to the Nth argument of RELATION.
N must satisfy INTEGERP.
Single value returned is a list of elements satisfying INDEXED-TERM-P.

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

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

function ALL-SPEC-ATTRIBUTES : (att &optional mt tv)
Returns all spec-attributes of attribute ATT
(descending transitive closure; expensive)
ATT must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

function ALL-SPEC-ATTRIBUTES-IF : (function att &optional mt tv)
Returns all genl-attributes of attribute ATT that satisfy FUNCTION
(FUNCTION must not effect sbhl search state)
FUNCTION must satisfy FUNCTION-SPEC-P.
ATT must satisfy EL-FORT-P.
Single value returned is a list of elements satisfying FORT-P.

2.7 Inference Module

Methods for the inference engine to query and modify the knowledge base. The FI- prefixed functions are deprecated.

function FI-FIND : (name)
Return the constant indentified by the string NAME.
Single value returned satisfies CONSTANT-P or is NIL.

function FI-COMPLETE : (prefix &optional case-sensitive?)
Return a list of constants whose name begins with PREFIX. The comparison is
performed in a case-insensitive mode unless CASE-SENSITIVE? is non-nil.
Single value returned is a list of elements satisfying CONSTANT-P.

function FI-CREATE : (name &optional external-id)
Create a new constant with NAME.
If EXTERNAL-ID is non-null it is used, otherwise a unique identifier is generated.
Single value returned satisfies CONSTANT-P.

function FI-FIND-OR-CREATE : (name &optional external-id)
Return constant with NAME if it is present.
If not present, then create constant with NAME, using EXTERNAL-ID if given.
If EXTERNAL-ID is not given, generate a new one for the new constant.
Single value returned satisfies CONSTANT-P.

function FI-KILL : (fort)
Kill FORT and all its uses from the KB. If FORT is a microtheory, all assertions
in that microtheory are removed.
Single value returned satisfies BOOLEANP.

function FI-RENAME : (constant name)
Change name of CONSTANT to NAME. Return the constant if no error, otherwise return NIL.
Single value returned satisfies CONSTANT-P or is NIL.

function FI-LOOKUP : (formula mt)
Returns two values when looking up the EL FORMULA in the microtheory MT. The
first value returned is a list of HL formulas resulting from the canonicalization
of the EL FORMULA. The second value is T iff all the HL assertions were properly
put into the KB.
Value 1 returned is a list of elements satisfying CONSP.
Value 2 returned satisfies BOOLEANP

function FI-ASSERT : (formula mt &optional strength direction)
Assert the FORMULA in the specified MT. STRENGTH is :default or :monotonic.
DIRECTION is :forward or :backward. GAF assertion direction defaults to :forward, and rule
assertion direction defaults to :backward. Return T if there was no error.
Single value returned satisfies BOOLEANP.

function FI-UNASSERT : (formula mt)
Remove the assertions canonicalized from FORMULA in the microtheory MT.
Return T if the operation succeeded, otherwise return NIL.
Single value returned satisfies BOOLEANP.

function FI-EDIT : (old-formula new-formula &optional old-mt new-mt strength direction)
Unassert the assertions canonicalized from OLD-FORMULA in the microtheory OLD-MT.
Assert NEW-FORMULA in the specified NEW-MT.
STRENGTH is :default or :monotonic.
DIRECTION is :forward or :backward.
GAF assertion direction defaults to :forward.
Rule assertion direction defaults to :backward.
Return T if there was no error.
Single value returned satisfies BOOLEANP.

function FI-BLAST : (formula mt)
Remove all arguments for the FORMULA within MT, including both those
arguments resulting the direct assertion of the FORMULA, and
those arguments supporting the FORMULA which were derived through inference.
Return T if successful, otherwise return NIL.
Single value returned satisfies BOOLEANP.

function FI-ASK : (formula &optional mt backchain number time depth)
Ask for bindings for free variables which will satisfy FORMULA within MT.
If BACKCHAIN is NIL, no inference is performed.
If BACKCHAIN is an integer, then at most that many backchaining steps using rules
are performed.
If BACKCHAIN is T, then inference is performed without limit on the number of
backchaining steps when searching for bindings.
If NUMBER is an integer, then at most that number of bindings are returned.
If TIME is an integer, then at most TIME seconds are consumed by the search for
bindings.
If DEPTH is an integer, then the inference paths are limited to that number of
total steps.
Returns NIL if the operation had an error. Otherwise returns a list of variable/
binding pairs. In the case where the FORMULA has no free variables, the form
(((T . T))) is returned indicating that the gaf is either directly asserted in the
KB, or that it can be derived via rules in the KB.
Single value returned satisfies LISTP or is NIL.

function FI-CONTINUE-LAST-ASK : (&optional backchain number time depth reconsider-deep)
Continue the last ask that was performed with more resources.
If BACKCHAIN is NIL, no inference is performed.
If BACKCHAIN is an integer, then at most that many backchaining steps using rules
are performed.
If BACKCHAIN is T, then inference is performed without limit on the number of
backchaining steps when searching for bindings.
If NUMBER is an integer, then at most that number of bindings are returned.
If TIME is an integer, then at most TIME seconds are consumed by the search for
bindings.
If DEPTH is an integer, then the inference paths are limited to that number of
total steps.
Returns NIL if the operation had an error. Otherwise returns a list of variable/
binding pairs. In the case where the FORMULA has no free variables, the form
(((T . T))) is returned indicating that the gaf is either directly asserted in the
KB, or that it can be derived via rules in the KB.
Single value returned satisfies LISTP or is NIL.

function FI-ASK-STATUS : ()
Return a status as to how the last ask successfully completed regarding
resource limits.
:EXHAUST if the search spaces was exhausted.
:DEPTH if the search space was limited because some nodes were too deep.
:NUMBER if the requested number of bindings was found without exceeding other limits.
:TIME if the time alloted expired prior to exhausting the search space.
Return NIL if there was no prior successful ask.
Single value returned satisfies ATOM or is NIL.

function FI-TMS-RECONSIDER-FORMULA : (formula mt)
Reconsider all arguments for FORMULA within MT. Return T if the
operation succeeded, NIL if there was an error.
Single value returned satisfies BOOLEANP.

function FI-TMS-RECONSIDER-MT : (mt)
Reconsider all arguments for all formulas within MT. Return T if the
operation succeeded, NIL if there was an error.
Single value returned satisfies BOOLEANP.

function FI-TMS-RECONSIDER-GAFS : (term &optional arg predicate mt)
Reconsider all arguments for all gaf formulas involving TERM.
ARG optionally constrains gafs such that the TERM occupies a specific arg position.
PREDICATE optionally constrains gafs such that the specifed PREDICATE
occupies the arg0 position.
MT optionally constrains gafs such that they must be included in the specific
microtheory.
Return T if the operation succeeded, NIL if there was an error.
Single value returned satisfies BOOLEANP.

function FI-TMS-RECONSIDER-TERM : (term &optional mt)
Reconsider all arguments involving TERM.
If MT is provided, then only arguments in that microtheory are reconsidered.
Return T if the operation succeeded, NIL if there was an error.
Single value returned satisfies BOOLEANP.

function FI-HYPOTHESIZE : (formula mt &optional name-prefix term-ids)
Cyc attempts to check if FORMULA is satisfiable in MT by 'hypothesizing'
constants for the variables in FORMULA, substituting them into FORMULA,
and asserting the new formula in MT. If this would trigger a
contradiction, then NIL is returned. Otherwise a binding list of variable /
constant pairs is returned, indicating the constants which were
successfully 'hypothesized'. The form (((T . T))) is returned if no new terms
required creation for the assertion of FORMULA.
NAME-PREFIX is a string which is used as a prefix for the name of each new
constant hypothesized. TERM-IDS is a list of variable / id pairs indicating
that the specified id should be used when generating the constant for the variable
in FORMULA. If TERM-IDS is NIL, then unused ids are allocated for the new
constants.
Single value returned satisfies LISTP or is NIL.

function FI-PROVE : (formula mt &optional backchain number time depth)
Attempts to prove FORMULA is true in MT under the given resource constraints.
BACKCHAIN, NUMBER, TIME and DEPTH function as described for FI-ASK.
FORMULA is interpreted as follows:
If FORMULA is of the form (#$implies [antecedant] [consequent]) then
(1) free variables in [antecedant] are assumed to be universally
quantified
(2) remaining variables in [consequent] are assumed to be existentially
quantified.
Otherwise FORMULA is interpreted as (#$implies #$True FORMULA) and handled as the
case above.
It returns NIL or a list of arguments as described for FI-JUSTIFY.
Single value returned satisfies (LIST LISTP) or is NIL.

function FI-GET-ERROR : ()
Return a description of the error resulting from the last FI operation.
Single value returned satisfies ATOM or is NIL.

function FI-GET-WARNING : ()
Return a description of the warning resulting from the last FI operation.
Single value returned satisfies ATOM or is NIL.

function CYC-FIND-OR-CREATE : (name external-id)
Return constant with NAME if it is present.
If not present, then create constant with NAME, using EXTERNAL-ID if given.
If EXTERNAL-ID is not given, generate a new one for the new constant.
NAME must satisfy VALID-CONSTANT-NAME.
EXTERNAL-ID must satisfy (NIL-OR CONSTANT-EXTERNAL-ID-P).
Single value returned satisfies CONSTANT-P.

function CYC-CREATE : (name external-id)
Create a new constant with id EXTERNAL-ID.
If NAME is anything other than :unnamed,
the new constant will be given the name NAME.
NAME must satisfy NEW-CONSTANT-NAME-SPEC-P.
EXTERNAL-ID must satisfy (NIL-OR CONSTANT-EXTERNAL-ID-P).
Single value returned satisfies CONSTANT-P.

function CYC-CREATE-NEW-EPHEMERAL : (name)
Creates a new constant with name NAME, but makes
no effort to synchronize its external ID with
other Cyc images. This is intended for constants
that will not be transmitted to other Cyc images.
NAME must satisfy NEW-CONSTANT-NAME-SPEC-P.
Single value returned satisfies CONSTANT-P.

function CYC-CREATE-NEW-PERMANENT : (name)
Creates a new constant with name NAME, gives it a
permanent unique external ID, and adds the constant
creation operation to the transcript queue.
NAME must satisfy NEW-CONSTANT-NAME-SPEC-P.
Single value returned satisfies CONSTANT-P.

function CYC-KILL : (fort)
Kill FORT and all its uses from the KB. If FORT is a microtheory, all assertions
in that microtheory are removed.
FORT must satisfy FORT-P.
Single value returned satisfies BOOLEANP.

function CYC-RECREATE : (constant)
Doesn't unassert the bookkeeping info,
but it might actually move it, or change
its format somehow.
CONSTANT must satisfy CONSTANT-P.
Single value returned satisfies CONSTANT-P.

function CYC-RENAME : (constant name)
Change name of CONSTANT to NAME. Return the constant if no error, otherwise return NIL.
CONSTANT must satisfy CONSTANT-P.
NAME must satisfy VALID-CONSTANT-NAME.
Single value returned satisfies CONSTANT-P or is NIL.

function CYC-MERGE : (kill-fort keep-fort)
Move asserted assertions on KILL-TERM onto KEEP-TERM before killing KILL-TERM.
@return fort-p; KEEP-FORT
KILL-FORT must satisfy FORT-P.
KEEP-FORT must satisfy FORT-P.
Single value returned satisfies FORT-P.

function CYC-ASSERT : (sentence &optional mt properties)
Assert SENTENCE in the specified MT.
properties; :strength el-strength-p (:default or :monotonic)
:direction direction-p (:forward or :backward)
GAF assertion direction defaults to :forward, and rule
assertion direction defaults to :backward.
@return booleanp; t iff the assert succeeded. If the assertion
already existed, it is considered a success.
SENTENCE must satisfy POSSIBLY-SENTENCE-P.
MT must satisfy (NIL-OR HLMT-P).
PROPERTIES must satisfy ASSERT-PROPERTIES-P.
Single value returned satisfies BOOLEANP.

function CYC-UNASSERT : (sentence &optional mt)
Remove the assertions canonicalized from FORMULA in the microtheory MT.
Return T if the operation succeeded, otherwise return NIL.
SENTENCE must satisfy POSSIBLY-SENTENCE-P.
MT must satisfy (NIL-OR HLMT-P).
Single value returned satisfies BOOLEANP.

function CYC-EDIT : (old-sentence new-sentence &optional old-mt new-mt properties)
Unassert OLD-SENTENCE in OLD-MT, and assert NEW-SENTENCE in the specified NEW-MT.
@see cyc-unassert and @xref cyc-assert
OLD-SENTENCE must satisfy POSSIBLY-SENTENCE-P.
NEW-SENTENCE must satisfy POSSIBLY-SENTENCE-P.
OLD-MT must satisfy (NIL-OR HLMT-P).
NEW-MT must satisfy (NIL-OR HLMT-P).
Single value returned satisfies BOOLEANP.

function CYC-QUERY : (sentence &optional mt properties)
Query for bindings for free variables which will satisfy SENTENCE within MT.
;;;{{{DOC
Properties: :backchain NIL or an integer or T
:number NIL or an integer
:time NIL or an integer
:depth NIL or an integer
:conditional-sentence boolean
If :backchain is NIL, no backchaining is performed.
If :backchain is an integer, then at most that many backchaining steps using rules
are performed.
If :backchain is T, then inference is performed without limit on the number of
backchaining steps when searching for bindings.
If :number is an integer, then at most that number of bindings are returned.
If :time is an integer, then at most that many seconds are consumed by the search for
bindings.
If :depth is an integer, then the inference paths are limited to that number of
total steps.
Returns NIL if the operation had an error. Otherwise returns a (possibly empty)
binding set. In the case where the SENTENCE has no free variables,
the form (NIL), the empty binding set is returned, indicating that the gaf is either
directly asserted in the KB, or that it can be derived via rules in the KB.
If it fails to be proven, NIL will be returned.
The second return value indicates the reason why the query halted.
If SENTENCE is an implication, or an ist wrapped around an implication,
and the :conditional-sentence property is non-nil, cyc-query will attempt to
prove SENTENCE by reductio ad absurdum.
;;;}}}EDOC
SENTENCE must satisfy POSSIBLY-SENTENCE-P.
MT must satisfy (NIL-OR HLMT-P).
PROPERTIES must satisfy QUERY-PROPERTIES-P.
Single value returned satisfies QUERY-RESULTS-P.

function CYC-CONTINUE-QUERY : (&optional query-id properties)
Continues a query started by @xref cyc-query.
If QUERY-ID is :last, the most recent query is continued.
QUERY-ID must satisfy QUERY-ID-P.
PROPERTIES must satisfy QUERY-PROPERTIES-P.
Single value returned satisfies QUERY-RESULTS-P.

function CYC-ADD-ARGUMENT : (sentence cycl-supports &optional mt properties verify-supports)
Tell Cyc to conclude SENTENCE (optionally in MT) based on the list of CYCL-SUPPORTS which should themselves be assertions or
otherwise valid for support-p. If VERIFY-SUPPORTS is non-nil, then this function will attempt to verify the list of supports
before making the assertion.
Properties: :direction :forward or :backward
SENTENCE must satisfy POSSIBLY-SENTENCE-P.
CYCL-SUPPORTS must satisfy LIST-OF-CYCL-SUPPORT-P.
MT must satisfy (NIL-OR HLMT-P).
PROPERTIES must satisfy ASSERT-PROPERTIES-P.
VERIFY-SUPPORTS must satisfy BOOLEANP.
Single value returned satisfies BOOLEANP.

function CYC-REMOVE-ALL-ARGUMENTS : (sentence &optional mt)
Remove all arguments for SENTENCE within MT, including both those
arguments resulting the direct assertion of SENTENCE, and
those arguments supporting SENTENCE which were derived through inference.
Return T if successful, otherwise return NIL.
SENTENCE must satisfy POSSIBLY-SENTENCE-P.
MT must satisfy (NIL-OR HLMT-P).
Single value returned satisfies BOOLEANP.

function CYC-REMOVE-ARGUMENT : (sentence cycl-supports &optional mt)
Remove the argument for SENTENCE specified by CYCL-SUPPORTS.
SENTENCE must satisfy POSSIBLY-SENTENCE-P.
CYCL-SUPPORTS must satisfy LIST-OF-CYCL-SUPPORT-P.
MT must satisfy (NIL-OR HLMT-P).
Single value returned satisfies BOOLEANP.

function CYC-REWRITE : (source-fort target-fort)
'moves' all asserted arguments from SOURCE-FORT to TARGET-FORT
@return fort-p; TARGET-FORT
SOURCE-FORT must satisfy FORT-P.
TARGET-FORT must satisfy FORT-P.
Single value returned satisfies FORT-P.

function CYC-TMS-RECONSIDER-SENTENCE : (sentence &optional mt)
Reconsider all arguments for SENTENCE within MT. Return T if the
operation succeeded, NIL if there was an error.
SENTENCE must satisfy POSSIBLY-SENTENCE-P.
MT must satisfy (NIL-OR HLMT-P).
Single value returned satisfies BOOLEANP.

3. Transport Layer

There are two transport protocols; the first is a convenient but incomplete telnet-like protocol, which is described in detail below. And the second is a complete binary protocol, named CFASL for which the reference client implementation is given by CfaslInputStream and CfaslOutputStream java classes. The source code for the reference java Cyc api client implementation is maintained at SourceForge.

3.1 TCP Ports

The Cyc server provides API services by binding two TCP ports and accepting TCP connections at those ports. The default installation installs API servers accepting at ports 3601 (ASCII) and 3614 (CFASL). The actual port numbers used can be specified at installation time.

3.1.1 TCP Port Security

The Cyc server does not provide secure tcp connections. Consequently it should be installed behind a network firewall or local firewall. Applications using Cyc should reside within the firewalled network or on the same host as Cyc. Remote access to Cyc should be performed using secure shell (SSH) to forward the ports Cyc uses, over an encrypted channel. Cyc's built in HTTP server defaults to port 8088 which can be proxied as a secure (HTTPS) internet service.

3.2 Establishing a connection

A client application establishs an API connection to a Cyc server by opening a TCP connection to one of the API ports on the machine running the Cyc server. The socket established is used to communicate API messages to Cyc and read results from Cyc.

For the default installation, a connection is thus established by opening a TCP connection to port 3601 or 3614 of the machine running the Cyc server.

3.3 Server Algorithm

Once the socket to be used for communication is established, the Cyc API server goes into a loop performing the following steps in order until the connection is closed :

input one API request from the socket
evaluate the request
output the result to the socket

The protocol of each step is described below for the ASCII communication mode.

3.4 ASCII Message protocols

All messages used to input an API request and output an API result are ASCII text messages. Input messages are sent from the client to the socket and at the Cyc server read from its input stream for the socket. Output messages are sent from the Cyc server to its output stream for the socket and are read from the socket by the client application.

The Cyc server flushes its output stream for the socket after each output message is sent in order to ensure the client application can read a complete output message without blocking.

The client application is similary reminded to flush its socket after each input message is sent in order to ensure the Cyc server can read a complete input message without blocking.

3.4.1 Input message protocol

The default input message protocol is an ASCII text message which can be read in from the socket using the SubL "read" protocol. More precisely, the SubL function READ is called on the input stream for the socket in order to produce a SubL form. This form represents the request to be evaluated.

Each API request is thus a textual sequence of the form

( <API function> <arg1> ... <argN> ) <whitespace>

For example :

(constant-id #$Thing)

The arguments to an API request may themselves be API requests. For example :

(constant-id (find-constant "Thing"))

3.4.2 Evaluating an API request

The API request read in is evaluated according to the SubL "eval" protocol. More precisely, the SubL function EVAL is called on the form in order to produce a single SubL result. This result is outputted using the output message protocol. If a function returns multiple values, only the first value is used, however the SubL function MULTIPLE-VALUE-LIST can be used to gather multiple values into a single list.

If an error condition occurs during evaluation, the evaluation is aborted and a string representing the error condition is used as the result of the evaluation.

3.4.3 Output message protocol

The default API output message protocol consists of two parts. First, a code is output indicating whether or not the API request succeeded or generated an error.

The code output is either the textual sequence

200 <whitespace>

for a successful evaluation, or the sequence

500 <whitespace>

if an error occurred during evaluation. This code can be used by the client application to interpret the second part of the output protocol.

Second, the result of the API request is output according to the SubL "print" protocol. More precisely, the SubL function PRINT is called on the result of the evaluation.

Thus, the result will be a textual sequence of the form

<API result> <whitespace>

3.5 Closing a connection

A client application closes an API connection to a Cyc server by simply executing the API request

(api-quit) <whitespace>

This will cause the Cyc server to halt the connection and close the socket.

3.6 Multithreading

In Cyc's multithreaded implementation, each API connection spawns a separate thread which is completely dedicated to handling the API server connection. When the connection is broken, the thread exits.

Note that a consequence of using a multithreaded implementation is that the Cyc process is always responsive to new TCP connections, and modifications to the Cyc KB performed via the API server are always reflected in future API connections.

3.7 Sample API session

As described above, the ASCII API protocol is telnet-like. As a result, one can in fact use 'telnet' or secure-shell to connect to a machine which is running a Cyc server that is providing API services. This is useful for debugging and remote administration.

Below is a trace of a simple API server session via 'telnet' to a Cyc server running on the machine foo.bar.com :

user@foo.bar.com ~$ telnet foo.bar.com 3601
Trying 207.207.8.15...
Connected to foo.bar.com.
Escape character is '^]'.
(fi-find "Fido")
200 NIL
(fi-create "Fido")
200 #$Fido
(fi-find "Fido")
200 #$Fido
(fi-assert '(#$isa #$Fido #$Dog) #$BaseKB)
200 T
(fi-ask '(#$isa #$Fido ?COL) #$BaseKB nil 2)
200 (((?COL . #$Dog)) ((?COL . #$DomesticPet)))
(fi-continue-last-ask nil 2)
200 (((?COL . #$DomesticatedAnimal)) ((?COL . #$TameAnimal)))
(fi-ask '(#$isa #$Fido #$Mammal) #$BaseKB nil 2)
200 (((T . T)))
(mapcar #'assertion-id (gather-arg-index #$Fido 1 #$isa #$BaseKB))
200 (664220)
(assertion-cnf (find-assertion-by-id 664220))
200 (NIL ((#$isa #$Fido #$Dog)))
(assertion-el-formula (find-assertion-by-id 664220))
200 (#$isa #$Fido #$Dog)
(fi-kill #$Fido)
200 T
(fi-find "Fido")
200 NIL
(api-quit)
Connection closed by foreign host.

Appendix A : Glossary

arg

Represents the ordinal argument number in a CycL expression of the form (Arg0 Arg1 ... ArgN). Arg 0 is distinguished as the predicate position.

argument

Is either a belief or a deduction that supports an assertion. Curently a belief results from a direct assertion. So an assertion is supported by either the fact that it was asserted by a Cyclist, it is supported by one or more applications of a rule assertion.

ask

A facility for querying the KB, obtaining bindings for variables in CycL EL formulas. Or obtaining confirmation that a ground formula is present in the KB.

assert

A facility for inputting facts and rules into the KB. Also known as Tell in the KB literature.

assertion

A CycL formula with or without variables (see GAF), which is present in the KB either through direct input by a Cyclist or as a result of inference from other assertions.

body

In Lisp macros, the body is a sequence of statements which define the expansion of the macro call into an evaluatable Lisp expression.

characterp

A predicate function which returns T if and only if the single argument is a character type.

Constant

A unique symbol within the KB. The meaning and usage of a Constant depends upon assertions containing it, within a particular microtheory. Lower level tools require that constants have the prefix #$ as in #$BaseKB, #$Thing, #$Collection, #$isa and #$implies.

Cyc

L The declarative language of the Cyc System in which assertions are written. CycL is derived from first-order predicate calculus, but includes many extensions to FOPC which enhance the expressiveness of the language.

deduction

A set of assertions which support a specific assertion. Also known as a Justification in the KB literature.

direction

An inference attribute of an assertion. Value :forward means that at the time of assertion, the inference engine uses the new assertion with all existing rules in applicable microtheories to derive additional assertions. Value :backward means that the the inference engine may use the new assertion to derive assertions when seeking bindings for an Ask operation. Rules default to :backward because they may otherwise potentially generate many uninteresting assertions. Gafs default to :forward because forward inference serves to derive likely useful additional assertions in a limited manner.

EL

An acronym for Epistemological Level which is a CycL representation optimized for human authoring and understanding. The canonicalizer facility of the KB automatically translates input formulas in EL form into efficient Heuristic Level (HL) representation. Likewise an uncanonicalizer facility generates EL formula from their HL counterpart representation. For example the logical operator #$implies is used at the EL, but the KB converts implications to Conjunctive Normal Form (CNF) at the HL.

FI

An acronym for the Functional Interface which is a small set of powerful high-level API functions. Remaining API functions provide efficient access to KB objects in particular situations. FI covers constant/assertion creation and removal from the KB as well as queries.

gaf

An acronym for Ground Atomic Formula which is an assertion without any variables. Gafs form the great majority of KB assertions. The Arg0 term in a gaf is the predicate.

genl

A CycL predicate meaning the generalization relationship of a specific KB collection to a more general collection.

formula

A formula is an expression following CycL syntax.

fort

An acronym for First Order Reified Term which is defined to be either a constant, or a reified Non-Atomic Reified Term (NART).

function

In the API context, this is a either a built in SubL procedure or one defined using SubL definition facilities.

HL

An acronym for Heuristic Level which is the efficient interal representation of KB datastructures and the procedures for accessing them.

hypothesize

A feature of the KB which allows a query to be answered by automatically instantiating any required constants.

id

A unique integer identifier for a KB item.

iff

If and only if.

indexed term

Those terms, arguments to CycL predicates or functions, which are suitable for indexing in the KB. The great majority of KB terms are indexed. Non indexed terms are primarily logical connectives, heavily used CycL predicates having alternate efficient access mechanisms, and unlikely query candidates such as numbers.

isa

A CycL predicate meaning membership in a collection.

KB

An acronym for Knowledge Base, specifically the Cyc server.

map

A SubL function which applies an argument SubL function over a set of objects, either to return a result or for a side-effect purpose.

macro

A SubL source code expansion facility.

mt

A acronym for Microtheory.

nart

A Non-Atomic Reified Term is a CycL term (argument to CycL predicate or function) which is neither a variable nor an atomic (one word) constant. NARTs are are terms formed by applying a CycL function to its arguments.

predicate

A CycL predicate is a term appearing in the Arg0 position of a GAF. The purpose of CycL predicates is to contain the meaning of constant relationships.

prove

A KB query returning a list of supporting arguments for the given formula, if it can be proven within the specified resource constraints.

rule

A CycL formula containing variables whose EL representation begins with #$implies. A rule has two parts, called its antecedent (left-hand side) and consequent (right-hand side).

search space

When performing a query operation, the search space denotes all the possible derived assertions, obtaining the total number of bindings for the query. The inference engine explores the search space, seeking bindings in an efficient fashion, limited by the given resource constraints.

sense

At the HL, sense distinguishes either the positive (via :pos) or negative (via :neg) clauses of an assertion represented in Conjunctive Normal Form.

string

A SubL object consisting of a sequence of characters.

support

A KB support is circumstance (represented by a variety of HL datastructures) affecting the belief in a particular assertion. Supports are linked to assertions via KB arguments.

strength

An assertion may have strength values from among the following: :default (true unless otherwise as an exception known to be false), :true (true because a user specifies it absolutely true), :unknown (truth value cannot be determined at this KB state).

tms

An acronym for Truth Maintenance System. The KB facility whereby previously derived assertions are automatically unasserted when KB supports are removed. TMS ensures a consistent KB when a supporting assertion is undone by the user.

truth

An assertion may have either the value :true or the value :false as its truth value. The great majority of KB assertions have truth value :true.

truth value

A composite assertion attribute for strength and truth attribute combinations. The truth value :true-mon means absolutely true. The truth value :true-def means true unless otherwise known to be false. The truth value :unknown means that the truth value is not known to be true and not known to be false. The truth value :false-def means false unless otherwise known to be true. And :false-mon means absolutely false.

variable

A type of CycL term appearing in rules standing for not-known-in-advance constants that satisfy the formula of a rule. When used in a KB query, variables specify which bindings are sought by the inference engine.

Appendix B : Index

A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

A

B

BACKWARD-ASSERTION? function
BINARY-PREDICATE? function

C

CLAUSE-EQUAL function
CLAUSE-LITERAL function
CLAUSE-P function
CLAUSE-WITHOUT-LITERAL function
CNF-FORMULA function
CNF-FORMULA-FROM-CLAUSES function
CNF-P function
CODE-ASSERTION? function
COLLECTION-LEAVES function
COLLECTIONS-COEXTENSIONAL? function
function

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