com.cyc.cycjava.cycl.inference.harness
Class inference_datastructures_proof
java.lang.Object
com.cyc.tool.subl.util.SubLTrampolineFile
com.cyc.tool.subl.util.SubLTranslatedFile
com.cyc.cycjava.cycl.inference.harness.inference_datastructures_proof
- All Implemented Interfaces:
- CommonSymbols, SubLFile
public final class inference_datastructures_proof
- extends SubLTranslatedFile
| Fields inherited from interface com.cyc.tool.subl.jrtl.nativeCode.subLisp.CommonSymbols |
ANSWER_TAG, APPEND_KEYWORD, APPEND_STACK_TRACES_TO_ERROR_MESSAGES, AREF, ASSEMBLE_FIXNUMS_TO_INTEGER, ATOM, BIGNUMP, BINARY_KEYWORD, BINDING_TYPE, BOOLEANP, CAAR, CADR, CAND, CAR, CCATCH, CDEC, CDESTRUCTURING_BIND, CDO, CDO_ALL_SYMBOLS, CDO_EXTERNAL_SYMBOLS, CDO_SYMBOLS, CDOHASH, CDOLIST, CDOTIMES, CDR, CHAR, CHAR_E_SYMBOL, CHAR_EQUAL_SYMBOL, CHAR_GREATER_THAN_OR_EQUAL_SYMBOL, CHAR_GREATER_THAN_SYMBOL, CHAR_GT_SYMBOL, CHAR_GTE_SYMBOL, CHAR_LESS_THAN_OR_EQUAL_SYMBOL, CHAR_LESS_THAN_SYMBOL, CHAR_LT_SYMBOL, CHAR_LTE_SYMBOL, CHAR_NE_SYMBOL, CHAR_NOT_EQUAL_SYMBOL, CHARACTERP, CHECK_TYPE, CINC, CLET, CMULTIPLE_VALUE_BIND, CNOT, CONS, CONSP, CONSTANT, COR, CPOP, CPROGV, CPUSH, CPUSHNEW, CREATE_KEYWORD, CSETF, CSETQ, CSOME, CTIME, CUNWIND_PROTECT, CVS_ID, DEBUG_IO, DECLAIM, DECLARE, DEFCONSTANT, DEFINE, DEFLEXICAL, DEFMACRO, DEFPARAMETER, DEFVAR, DIRECTION_KEYWORD, DYNAMIC, EIGHT_INTEGER, EIGHTEEN_INTEGER, ELEMENT_TYPE_KEYWORD, ELEVEN_INTEGER, END_KEYWORD, ENFORCE_MUST, ENFORCE_TYPE, EQ, EQL, EQUAL, EQUALP, ERROR, ERROR_KEYWORD, ERROR_OUTPUT, EVAL, EXTERNAL_FORMAT_KEYWORD, EXTERNAL_KEYWORD, FIF, FIFTEEN_INTEGER, FIRST, FIVE_INTEGER, FIXNUMP, FLOATP, FOUR_INTEGER, FOURTEEN_INTEGER, FUNCTION, FUNCTION_SPEC_P, FUNCTIONP, FUNLESS, FWHEN, GET, GETHASH, GETHASH_WITHOUT_VALUES, GUID_P, HASH_TABLE_ITERATOR_P, HASH_TABLE_P, IDENTITY, IF_DOES_NOT_EXIST_KEYWORD, IF_EXISTS_KEYWORD, IGNORE, INITIALIZATION_TYPE, INITIALIZER, INPUT_KEYWORD, INPUT_STREAM_P, INTEGERP, INTERNAL_KEYWORD, IO_KEYWORD, KEYWORDP, KILL_KEYWORD, LAMBDA_SYMBOL, LEXICAL, LIST, LISTP, LISTS, LOCK_P, LONG_BIGNUM_P, MACRO_ENV, MACRO_FORM, MEDIUM_BIGNUM_P, MEMBER, MINUS_ONE_INTEGER, MULTIPLE_VALUE_LIST, MUST, NCONC, NEW_VERSION_KEYWORD, NIL, NINE_INTEGER, NINETEEN_INTEGER, NREVERSE, NTH, NTH_VALUE, NULL, NULL_INPUT, NULL_OUTPUT, NUM_E_SYMBOL, NUM_GT_SYMBOL, NUM_GTE_SYMBOL, NUM_LT_SYMBOL, NUM_LTE_SYMBOL, NUM_NE_SYMBOL, NUMBERP, ONE_HUNDRED_THIRTY_SEVEN_INTEGER, ONE_HUNDRED_TWENTY_SEVEN_INTEGER, ONE_INTEGER, ONE_THOUSAND_INTEGER, OPTIONAL_SYMBOL, OTHERWISE, OUTPUT_KEYWORD, OUTPUT_STREAM_P, OVERWRITE_KEYWORD, PACKAGEP, PCASE, PCOND, PIF, PROBE_KEYWORD, PROCESS_TO_END, PROCESSP, PROCLAIM, PROGN, PUNLESS, PWHEN, QUERY_IO, QUIT, QUOTE, RENAME_AND_DELETE_KEYWORD, REST_SYMBOL, RET, RET_NIL, RET_T, RETURN_TAG, REVERSE, RW_LOCK_P, SECOND, SEQUENCEP, SEVEN_INTEGER, SEVENTEEN_INTEGER, SHORT_BIGNUM_P, SHOW_STACK_TRACES, SIX_INTEGER, SIXTEEN_INTEGER, SIXTY_FOUR_INTEGER, SORT, SSS, STANDARD_INPUT, STANDARD_OUTPUT, START_KEYWORD, STREAMP, STRING_E_SYMBOL, STRING_EQUAL_SYMBOL, STRING_GREATER_THAN_OR_EQUAL_SYMBOL, STRING_GREATER_THAN_SYMBOL, STRING_GT_SYMBOL, STRING_GTE_SYMBOL, STRING_LESS_THAN_OR_EQUAL_SYMBOL, STRING_LESS_THAN_SYMBOL, STRING_LT_SYMBOL, STRING_LTE_SYMBOL, STRING_NE_SYMBOL, STRING_NOT_EQUAL_SYMBOL, STRINGP, STRUCTURE_P, SUPERSEDE_KEYWORD, SUSPEND_TYPE_CHECKING, SYMBOL_FUNCTION, SYMBOL_VALUE, SYMBOLP, T, TEN_INTEGER, TERMINAL_IO, TEXT_KEYWORD, THIRTEEN_INTEGER, THIRTY_FOUR_INTEGER, THIRTY_THREE_INTEGER, THIRTY_TWO_INTEGER, THREE_INTEGER, TRACE_OUTPUT, TRUE, TWELVE_INTEGER, TWENTY_INTEGER, TWO_HUNDRED_FIFTY_FOUR_INTEGER, TWO_HUNDRED_FORTY_FOUR_INTEGER, TWO_INTEGER, UNDECLARED, UNPROVIDED, VALUES, VECTOR, VECTORP, WITH_ERROR_HANDLER, WITH_STATIC_AREA, WITH_THREAD_PRIVATE_AREA, WITH_WORKING_AREA, WORLD, ZERO_DOUBLE, ZERO_INTEGER |
|
Method Summary |
static SubLObject |
_csetf_prf_bindings(SubLObject object,
SubLObject value)
|
static SubLObject |
_csetf_prf_dependents(SubLObject object,
SubLObject value)
|
static SubLObject |
_csetf_prf_link(SubLObject object,
SubLObject value)
|
static SubLObject |
_csetf_prf_subproofs(SubLObject object,
SubLObject value)
|
static SubLObject |
_csetf_prf_suid(SubLObject object,
SubLObject value)
|
static SubLObject |
all_proof_subproofs_recursive(SubLObject proof,
SubLObject all_subproofs_set)
|
static SubLObject |
all_proof_subproofs(SubLObject proof)
|
static SubLObject |
declare_inference_datastructures_proof_file()
|
void |
declareFunctions()
Declares the mapping between functions and symbols for all named
functions defined in the file. |
static SubLObject |
destroy_problem_store_proof(SubLObject proof)
|
static SubLObject |
destroy_proof_int(SubLObject proof)
|
static SubLObject |
init_inference_datastructures_proof_file()
|
void |
initializeVariables()
Initializes all global variables and private internal variables
for constants defined in the file. |
static SubLObject |
make_proof(SubLObject arglist)
|
static SubLObject |
new_proof_with_bindings(SubLObject link,
SubLObject v_bindings,
SubLObject subproofs)
|
static SubLObject |
new_proof(SubLObject link,
SubLObject subproofs)
|
static SubLObject |
note_proof_invalid(SubLObject proof)
|
static SubLObject |
prf_bindings(SubLObject object)
|
static SubLObject |
prf_link(SubLObject object)
|
static SubLObject |
prf_subproofs(SubLObject object)
|
static SubLObject |
prf_suid(SubLObject object)
|
static SubLObject |
proof_bindings(SubLObject proof)
Maps PROOF's problem-query -> HL proven-query of PROOF
or equivalently, PROOF's problem-query vars -> content. |
static SubLObject |
proof_direct_subproofs(SubLObject proof)
|
static SubLObject |
proof_direct_supports_recursive(SubLObject proof)
|
static SubLObject |
proof_direct_supports(SubLObject proof)
|
static SubLObject |
proof_first_subproof(SubLObject proof)
|
static SubLObject |
proof_has_subproofsP(SubLObject proof)
|
static SubLObject |
proof_invalid_p(SubLObject proof)
|
static SubLObject |
proof_link(SubLObject proof)
|
static SubLObject |
proof_matches_specificationP(SubLObject candidate_proof,
SubLObject supported_problem,
SubLObject proof_bindings,
SubLObject proof_direct_supports)
|
static SubLObject |
proof_p(SubLObject object)
|
static SubLObject |
proof_print_function_trampoline(SubLObject object,
SubLObject stream)
|
static SubLObject |
proof_provenP(SubLObject proof)
|
static SubLObject |
proof_rejectedP(SubLObject proof)
|
static SubLObject |
proof_spec_direct_supports_recursive(SubLObject link,
SubLObject subproofs)
|
static SubLObject |
proof_spec_direct_supports(SubLObject link,
SubLObject subproofs)
|
static SubLObject |
proof_status(SubLObject proof)
|
static SubLObject |
proof_store(SubLObject proof)
|
static SubLObject |
proof_suid(SubLObject proof)
|
static SubLObject |
proof_supported_problem(SubLObject proof)
|
static SubLObject |
proof_supports(SubLObject proof)
|
static SubLObject |
proof_type(SubLObject proof)
|
static SubLObject |
register_proof(SubLObject proof)
Adds backpointers to PROOF from other datastructures |
void |
runTopLevelForms()
Runs all top-level forms in order. |
static SubLObject |
set_proof_bindings(SubLObject proof,
SubLObject v_bindings)
|
static SubLObject |
setup_inference_datastructures_proof_file()
|
static SubLObject |
valid_proof_p(SubLObject object)
|
| Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
me
public static final SubLFile me
myName
public static final java.lang.String myName
- See Also:
- Constant Field Values
$proof_datastructure_stores_dependent_proofsP$
public static SubLSymbol $proof_datastructure_stores_dependent_proofsP$
- If T, when a proof A is made a subproof of another proof B, the proof B is also recorded in the dependents slot the subproof A.
$dtp_proof$
public static SubLSymbol $dtp_proof$
$sym0$PROOF
public static final SubLSymbol $sym0$PROOF
$sym1$PROOF_P
public static final SubLSymbol $sym1$PROOF_P
$int2$211
public static final SubLInteger $int2$211
$list3
public static final SubLList $list3
$list4
public static final SubLList $list4
$list5
public static final SubLList $list5
$list6
public static final SubLList $list6
$sym7$PRINT_PROOF
public static final SubLSymbol $sym7$PRINT_PROOF
$sym8$PROOF_PRINT_FUNCTION_TRAMPOLINE
public static final SubLSymbol $sym8$PROOF_PRINT_FUNCTION_TRAMPOLINE
$sym9$PRF_SUID
public static final SubLSymbol $sym9$PRF_SUID
$sym10$_CSETF_PRF_SUID
public static final SubLSymbol $sym10$_CSETF_PRF_SUID
$sym11$PRF_BINDINGS
public static final SubLSymbol $sym11$PRF_BINDINGS
$sym12$_CSETF_PRF_BINDINGS
public static final SubLSymbol $sym12$_CSETF_PRF_BINDINGS
$sym13$PRF_LINK
public static final SubLSymbol $sym13$PRF_LINK
$sym14$_CSETF_PRF_LINK
public static final SubLSymbol $sym14$_CSETF_PRF_LINK
$sym15$PRF_SUBPROOFS
public static final SubLSymbol $sym15$PRF_SUBPROOFS
$sym16$_CSETF_PRF_SUBPROOFS
public static final SubLSymbol $sym16$_CSETF_PRF_SUBPROOFS
$sym17$PRF_DEPENDENTS
public static final SubLSymbol $sym17$PRF_DEPENDENTS
$sym18$_CSETF_PRF_DEPENDENTS
public static final SubLSymbol $sym18$_CSETF_PRF_DEPENDENTS
$kw19$SUID
public static final SubLSymbol $kw19$SUID
$kw20$BINDINGS
public static final SubLSymbol $kw20$BINDINGS
$kw21$LINK
public static final SubLSymbol $kw21$LINK
$kw22$SUBPROOFS
public static final SubLSymbol $kw22$SUBPROOFS
$kw23$DEPENDENTS
public static final SubLSymbol $kw23$DEPENDENTS
$str24$Invalid_slot__S_for_construction_
public static final SubLString $str24$Invalid_slot__S_for_construction_
$kw25$FREE
public static final SubLSymbol $kw25$FREE
$str26$_Invalid_PROOF__s_
public static final SubLString $str26$_Invalid_PROOF__s_
$sym27$PROOF_SUID
public static final SubLSymbol $sym27$PROOF_SUID
$str28$_PROOF__a__a_for_link__a__a_suppo
public static final SubLString $str28$_PROOF__a__a_for_link__a__a_suppo
$sym29$SXHASH_PROOF_METHOD
public static final SubLSymbol $sym29$SXHASH_PROOF_METHOD
$list30
public static final SubLList $list30
$sym31$DO_LIST
public static final SubLSymbol $sym31$DO_LIST
$sym32$PROOF_DIRECT_SUBPROOFS
public static final SubLSymbol $sym32$PROOF_DIRECT_SUBPROOFS
$list33
public static final SubLList $list33
$list34
public static final SubLList $list34
$kw35$ALLOW_OTHER_KEYS
public static final SubLSymbol $kw35$ALLOW_OTHER_KEYS
$kw36$DONE
public static final SubLSymbol $kw36$DONE
$sym37$ALL_PROOF_SUBPROOFS
public static final SubLSymbol $sym37$ALL_PROOF_SUBPROOFS
$list38
public static final SubLList $list38
$list39
public static final SubLList $list39
$kw40$PROOF_STATUS
public static final SubLSymbol $kw40$PROOF_STATUS
$sym41$PROOF_PROBLEM
public static final SubLSymbol $sym41$PROOF_PROBLEM
$sym42$SUPPORTED_PROBLEM
public static final SubLSymbol $sym42$SUPPORTED_PROBLEM
$sym43$DEPENDENT_PROOF
public static final SubLSymbol $sym43$DEPENDENT_PROOF
$sym44$CLET
public static final SubLSymbol $sym44$CLET
$sym45$PROOF_SUPPORTED_PROBLEM
public static final SubLSymbol $sym45$PROOF_SUPPORTED_PROBLEM
$sym46$DO_PROBLEM_SUPPORTED_PROBLEMS
public static final SubLSymbol $sym46$DO_PROBLEM_SUPPORTED_PROBLEMS
$sym47$DO_PROBLEM_PROOFS
public static final SubLSymbol $sym47$DO_PROBLEM_PROOFS
$sym48$PWHEN
public static final SubLSymbol $sym48$PWHEN
$sym49$MEMBER_EQ_
public static final SubLSymbol $sym49$MEMBER_EQ_
$sym50$CSOME
public static final SubLSymbol $sym50$CSOME
$sym51$PROOF_DEPENDENTS
public static final SubLSymbol $sym51$PROOF_DEPENDENTS
$sym52$PROOF_HAS_STATUS_
public static final SubLSymbol $sym52$PROOF_HAS_STATUS_
$sym53$PIF
public static final SubLSymbol $sym53$PIF
$sym54$_PROOF_DATASTRUCTURE_STORES_DEPENDENT_PROOFS__
public static final SubLSymbol $sym54$_PROOF_DATASTRUCTURE_STORES_DEPENDENT_PROOFS__
$sym55$DO_PROOF_DEPENDENT_PROOFS_INT
public static final SubLSymbol $sym55$DO_PROOF_DEPENDENT_PROOFS_INT
$sym56$DO_PROOF_DEPENDENT_PROOFS_COMPUTED
public static final SubLSymbol $sym56$DO_PROOF_DEPENDENT_PROOFS_COMPUTED
$sym57$PROBLEM_LINK_P
public static final SubLSymbol $sym57$PROBLEM_LINK_P
$sym58$LIST_OF_PROOF_P
public static final SubLSymbol $sym58$LIST_OF_PROOF_P
$sym59$BINDING_LIST_P
public static final SubLSymbol $sym59$BINDING_LIST_P
$str60$Could_not_remove_dependent__a_fro
public static final SubLString $str60$Could_not_remove_dependent__a_fro
$str61$Expected_link__a_to_have_exactly_
public static final SubLString $str61$Expected_link__a_to_have_exactly_
$str62$Unexpected_link_type_for_proof___
public static final SubLString $str62$Unexpected_link_type_for_proof___
$sym63$SUPPORT_EQUAL
public static final SubLSymbol $sym63$SUPPORT_EQUAL
$str64$Expected__s_to_have_at_most_one_s
public static final SubLString $str64$Expected__s_to_have_at_most_one_s
$sym65$_
public static final SubLSymbol $sym65$_
$sym66$PROBLEM_SUID
public static final SubLSymbol $sym66$PROBLEM_SUID
$kw67$REJECTED
public static final SubLSymbol $kw67$REJECTED
$kw68$PROVEN
public static final SubLSymbol $kw68$PROVEN
$sym69$PROOF_REJECT_REASON_P
public static final SubLSymbol $sym69$PROOF_REJECT_REASON_P
$kw70$ILL_FORMED
public static final SubLSymbol $kw70$ILL_FORMED
$sym71$PROBLEM_P
public static final SubLSymbol $sym71$PROBLEM_P
proof_print_function_trampoline
public static final SubLObject proof_print_function_trampoline(SubLObject object,
SubLObject stream)
proof_p
public static final SubLObject proof_p(SubLObject object)
prf_suid
public static final SubLObject prf_suid(SubLObject object)
prf_bindings
public static final SubLObject prf_bindings(SubLObject object)
prf_link
public static final SubLObject prf_link(SubLObject object)
prf_subproofs
public static final SubLObject prf_subproofs(SubLObject object)
_csetf_prf_suid
public static final SubLObject _csetf_prf_suid(SubLObject object,
SubLObject value)
_csetf_prf_bindings
public static final SubLObject _csetf_prf_bindings(SubLObject object,
SubLObject value)
_csetf_prf_link
public static final SubLObject _csetf_prf_link(SubLObject object,
SubLObject value)
_csetf_prf_subproofs
public static final SubLObject _csetf_prf_subproofs(SubLObject object,
SubLObject value)
_csetf_prf_dependents
public static final SubLObject _csetf_prf_dependents(SubLObject object,
SubLObject value)
make_proof
public static final SubLObject make_proof(SubLObject arglist)
valid_proof_p
public static final SubLObject valid_proof_p(SubLObject object)
proof_invalid_p
public static final SubLObject proof_invalid_p(SubLObject proof)
new_proof
public static final SubLObject new_proof(SubLObject link,
SubLObject subproofs)
new_proof_with_bindings
public static final SubLObject new_proof_with_bindings(SubLObject link,
SubLObject v_bindings,
SubLObject subproofs)
register_proof
public static final SubLObject register_proof(SubLObject proof)
- Adds backpointers to PROOF from other datastructures
destroy_problem_store_proof
public static final SubLObject destroy_problem_store_proof(SubLObject proof)
destroy_proof_int
public static final SubLObject destroy_proof_int(SubLObject proof)
note_proof_invalid
public static final SubLObject note_proof_invalid(SubLObject proof)
proof_suid
public static final SubLObject proof_suid(SubLObject proof)
proof_bindings
public static final SubLObject proof_bindings(SubLObject proof)
- Maps PROOF's problem-query -> HL proven-query of PROOF
or equivalently, PROOF's problem-query vars -> content.
Bindings to substitute into the supported-problem-query to get the proven-query.
First elements are variables in the supported-problem-query,
second elements are terms bound by this proof.
proof_link
public static final SubLObject proof_link(SubLObject proof)
proof_direct_subproofs
public static final SubLObject proof_direct_subproofs(SubLObject proof)
set_proof_bindings
public static final SubLObject set_proof_bindings(SubLObject proof,
SubLObject v_bindings)
proof_store
public static final SubLObject proof_store(SubLObject proof)
proof_supported_problem
public static final SubLObject proof_supported_problem(SubLObject proof)
proof_supports
public static final SubLObject proof_supports(SubLObject proof)
proof_spec_direct_supports
public static final SubLObject proof_spec_direct_supports(SubLObject link,
SubLObject subproofs)
proof_direct_supports_recursive
public static final SubLObject proof_direct_supports_recursive(SubLObject proof)
proof_spec_direct_supports_recursive
public static final SubLObject proof_spec_direct_supports_recursive(SubLObject link,
SubLObject subproofs)
proof_has_subproofsP
public static final SubLObject proof_has_subproofsP(SubLObject proof)
proof_first_subproof
public static final SubLObject proof_first_subproof(SubLObject proof)
- Returns:
- nil or proof-p
all_proof_subproofs
public static final SubLObject all_proof_subproofs(SubLObject proof)
all_proof_subproofs_recursive
public static final SubLObject all_proof_subproofs_recursive(SubLObject proof,
SubLObject all_subproofs_set)
proof_status
public static final SubLObject proof_status(SubLObject proof)
- Returns:
- proof-status-p
proof_rejectedP
public static final SubLObject proof_rejectedP(SubLObject proof)
proof_provenP
public static final SubLObject proof_provenP(SubLObject proof)
proof_type
public static final SubLObject proof_type(SubLObject proof)
- Returns:
- hl-module-p or problem-link-type-p
proof_matches_specificationP
public static final SubLObject proof_matches_specificationP(SubLObject candidate_proof,
SubLObject supported_problem,
SubLObject proof_bindings,
SubLObject proof_direct_supports)
- Returns:
- boolean; t iff CANDIDATE-PROOF would equal a proof supporting
SUPPORTED-PROBLEM, with bindings PROOF-BINDINGS and direct supports PROOF-DIRECT-SUPPORTS.
proof_direct_supports
public static final SubLObject proof_direct_supports(SubLObject proof)
declare_inference_datastructures_proof_file
public static final SubLObject declare_inference_datastructures_proof_file()
init_inference_datastructures_proof_file
public static final SubLObject init_inference_datastructures_proof_file()
setup_inference_datastructures_proof_file
public static final SubLObject setup_inference_datastructures_proof_file()
declareFunctions
public void declareFunctions()
- Description copied from interface:
SubLFile
- Declares the mapping between functions and symbols for all named
functions defined in the file.
Like CRTL define.
initializeVariables
public void initializeVariables()
- Description copied from interface:
SubLFile
- Initializes all global variables and private internal variables
for constants defined in the file.
Like CRTL init.
runTopLevelForms
public void runTopLevelForms()
- Description copied from interface:
SubLFile
- Runs all top-level forms in order.
Like CRTL setup.