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.