clausifier

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

com.cyc.cycjava.cycl
Class clausifier

java.lang.Object
  com.cyc.tool.subl.util.SubLTrampolineFile
      com.cyc.tool.subl.util.SubLTranslatedFile
          com.cyc.cycjava.cycl.clausifier

All Implemented Interfaces:: CommonSymbols, SubLFile

public final class clausifier
extends SubLTranslatedFile
extends SubLTranslatedFile

Nested Class Summary
`static class`	`clausifier.$conjunctions_in$UnaryFunction`
`static class`	`clausifier.$do_implications$UnaryFunction`
`static class`	`clausifier.$do_negations_destructive$UnaryFunction`
`static class`	`clausifier.$recursively_standardize_variables$UnaryFunction`
`static class`	`clausifier.$universals_out$UnaryFunction`

Nested classes/interfaces inherited from class com.cyc.tool.subl.util.SubLTranslatedFile
`SubLTranslatedFile.SubL`

Field Summary
`static SubLSymbol`	$canonical_variable_name_stem$ used for standardizing EL variables in the canonicalizer
`static SubLObject`	`$const12$DifferenceFn`
`static SubLObject`	`$const14$PlusFn`
`static SubLObject`	`$const18$Quote`
`static SubLObject`	`$const30$forAll`
`static SubLObject`	`$const38$thereExists`
`static SubLObject`	`$const39$SkolemFunctionFn`
`static SubLObject`	`$const6$True`
`static SubLObject`	`$const65$and`
`static SubLObject`	`$const7$False`
`static SubLInteger`	`$int16$32`
`static SubLInteger`	`$int49$200000`
`static SubLInteger`	`$int70$48`
`static SubLSymbol`	`$kw1$ERROR`
`static SubLSymbol`	`$kw2$UNINITIALIZED`
`static SubLSymbol`	`$kw22$IGNORE`
`static SubLSymbol`	`$kw25$TOO_MANY_SEQUENCE_VARS_IN_SKOLEM_SCOPE`
`static SubLSymbol`	`$kw26$AMBIGUOUS_VAR_TYPE_IN_SKOLEM_SCOPE`
`static SubLSymbol`	`$kw27$QUANTIFIED_SEQUENCE_VARIABLE`
`static SubLSymbol`	`$kw31$NEITHER`
`static SubLSymbol`	`$kw32$TERM`
`static SubLSymbol`	`$kw33$SEQ`
`static SubLSymbol`	`$kw34$BOTH`
`static SubLSymbol`	`$kw35$UNDETERMINED`
`static SubLSymbol`	`$kw41$ASSERT_ONLY`
`static SubLSymbol`	`$kw48$BAD_EXPONENTIAL_DISJUNCTION`
`static SubLSymbol`	`$kw5$HELLO_YOU_SILLY_COMPILER`
`static SubLSymbol`	`$kw56$BAD_EXPONENTIAL_CONJUNCTION`
`static SubLSymbol`	`$kw66$CNF`
`static SubLSymbol`	`$kw67$DNF`
`static SubLSymbol`	`$kw71$_MEMOIZED_ITEM_NOT_FOUND_`
`static SubLSymbol`	`$kw8$REGULARIZE`
`static SubLString`	`$str0$el_var`
`static SubLString`	`$str13$_s_contained_the_invalid_bound__D`
`static SubLString`	`$str23$_`
`static SubLString`	`$str29$Unexpected_sentence_type_in_exist`
`static SubLString`	`$str36$Skolemizer_failed_to_classify_var`
`static SubLString`	`$str37$skolem_constants_not_yet_supporte`
`static SubLString`	`$str40$make_skolem_fn_fn_doesn_t_know_ho`
`static SubLString`	`$str42$Unexpected_value_for__forbid_quan`
`static SubLString`	`$str44$Got_the_unexpected_sentence__S_in`
`static SubLString`	`$str46$Got_the_unexpected_sentence__S_in`
`static SubLString`	`$str51$_s_is_not_a_conjunction__so_it_is`
`static SubLString`	`$str52$_s_is_not_a_disjunction__so__S_is`
`static SubLString`	`$str54$Got_the_unexpected_formula__S_in_`
`static SubLString`	`$str57$_s_is_not_a_disjunction__so_it_is`
`static SubLString`	`$str58$_s_is_not_a_conjunction__so__S_is`
`static SubLString`	`$str9$_s_is_not_a_quantified_sentence`
`static SubLSymbol`	`$sym10$NEGATE_NEGATION`
`static SubLSymbol`	`$sym11$NEGATE_FORMULA`
`static SubLSymbol`	`$sym15$EL_FORMULA_P`
`static SubLSymbol`	`$sym17$CYC_VAR_`
`static SubLSymbol`	`$sym19$RECURSIVELY_STANDARDIZE_VARIABLES`
`static SubLSymbol`	`$sym20$EL_UNIQUIFY_STANDARDIZE`
`static SubLSymbol`	`$sym21$EL_VAR_WITHOUT_QUOTE`
`static SubLSymbol`	`$sym24$CYC_CONST_GENERAL_EXISTENTIAL_OPERATOR_P`
`static SubLSymbol`	`$sym28$EXISTENTIALS_OUT_INT`
`static SubLSymbol`	`$sym3$DO_IMPLICATIONS_RECURSIVE`
`static SubLSymbol`	`$sym4$DO_NEGATIONS_DESTRUCTIVE`
`static SubLSymbol`	`$sym43$UNIVERSALS_OUT`
`static SubLSymbol`	`$sym45$DISJUNCTIONS_IN`
`static SubLSymbol`	`$sym47$EL_CONJUNCTION_P`
`static SubLSymbol`	`$sym50$FORMULA_ARITY`
`static SubLSymbol`	`$sym53$CONJUNCTIONS_IN`
`static SubLSymbol`	`$sym55$EL_DISJUNCTION_P`
`static SubLSymbol`	`$sym59$PACKAGE_XNF_CLAUSE`
`static SubLSymbol`	`$sym60$FORMULA_ARG1`
`static SubLSymbol`	`$sym61$EL_VAR_`
`static SubLSymbol`	`$sym62$LEADING_UNIVERSAL_VARIABLES_1`
`static SubLSymbol`	`$sym63$STRING_`
`static SubLSymbol`	`$sym64$STR`
`static SubLSymbol`	`$sym68$CACHED_CNF_CLAUSAL_FORM`
`static SubLSymbol`	`$sym69$_CACHED_CNF_CLAUSAL_FORM_CACHING_STATE_`
`static SubLSymbol`	$use_cnf_cacheP$ Whether to cache the function that converts EL sentences to CNF clausal form
`static SubLFile`	`me`
`static java.lang.String`	`myName`

Fields inherited from class com.cyc.tool.subl.util.SubLTranslatedFile
`EMPTY_SUBL_OBJECT_ARRAY`

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

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`	`assume_free_vars_are_existentially_boundP()`
`static SubLObject`	`bad_exponential_conjunctionP(SubLObject sentence)`
`static SubLObject`	`bad_exponential_disjunctionP(SubLObject sentence)`
`static SubLObject`	`bad_exponential_sentenceP(SubLObject sentence, SubLObject arg_test_func)`
`static SubLObject`	`canon_fast_gafP(SubLObject sentence, SubLObject mt)`
`static SubLObject`	`clear_cached_cnf_clausal_form()`
`static SubLObject`	`cnf_clausal_form_int(SubLObject sentence, SubLObject mt)`
`static SubLObject`	`cnf_clausal_form(SubLObject sentence, SubLObject mt)`
`static SubLObject`	`cnf_operators_out(SubLObject sentence)`
`static SubLObject`	`conjunctions_in_int(SubLObject sentence)` Moves conjunctions inwards inside SENTENCE by repeatedly applying the following transformation: (#$and (#$or )) becomes (#$or (#$and ) (#$and )).
`static SubLObject`	`conjunctions_in(SubLObject sentence)`
`static SubLObject`	`czer_explicitify_implicit_quantifiers(SubLObject sentence)`
`static SubLObject`	`czer_explicitify_implicit_universal_quantifiers(SubLObject sentence)` Wraps SENTENCE in #$forAll statements (if needed) to quantify all the free variables within SENTENCE.
`static SubLObject`	`declare_clausifier_file()`
`void`	`declareFunctions()` Declares the mapping between functions and symbols for all named functions defined in the file.
`static SubLObject`	`determine_skolem_var_status(SubLObject var, SubLObject subsent_free_term_vars, SubLObject free_term_vars_in_scope, SubLObject subsent_free_seqvars, SubLObject free_seqvars_in_scope)`
`static SubLObject`	`disjunctions_in_int(SubLObject sentence)` Moves disjunctions inwards inside SENTENCE by repeatedly applying the following transformation: (#$or (#$and )) becomes (#$and (#$or ) (#$or )).
`static SubLObject`	`disjunctions_in(SubLObject sentence)`
`static SubLObject`	`dnf_operators_out(SubLObject sentence)`
`static SubLObject`	`do_implications_recursive(SubLObject sentence)` Removes all implications and equivalences from SENTENCE, returning a logically equivalent sentence.
`static SubLObject`	`do_implications(SubLObject sentence)`
`static SubLObject`	`do_negations_destructive(SubLObject sentence)` A destructive version of @xref do-negations.
`static SubLObject`	`drop_all_existentialsP()`
`static SubLObject`	`el_cnf_destructive(SubLObject sentence, SubLObject mt)` Destructively transforms an EL sentence into conjunctive normal form.
`static SubLObject`	`el_cnf_int(SubLObject sentence, SubLObject mt, SubLObject destructiveP)` Assumes the EL variable namespace is bound.
`static SubLObject`	`el_cnf(SubLObject sentence, SubLObject mt)` Constructively transforms an EL sentence into conjunctive normal form.
`static SubLObject`	`el_dnf_destructive(SubLObject sentence, SubLObject mt)` Destructively transforms an EL sentence into disjunctive normal form.
`static SubLObject`	`el_dnf_int(SubLObject sentence, SubLObject mt, SubLObject destructiveP)` Assumes the EL variable namespace is bound.
`static SubLObject`	`el_uniquify_standardize(SubLObject var)`
`static SubLObject`	`el_uniquify(SubLObject var)` Assumes that el-symbol-suffix-table is bound.
`static SubLObject`	`el_var_without_quote(SubLObject var)`
`static SubLObject`	`el_xnf_int(SubLObject sentence, SubLObject mt)`
`static SubLObject`	`el_xnf(SubLObject sentence, SubLObject mt)` Transforms an EL sentence so that it is ready to be put into either CNF or DNF form.
`static SubLObject`	`existentials_out_int(SubLObject sentence)` Removes all existentials by replacing them with Skolem constants or Skolem sentences.
`static SubLObject`	`existentials_out(SubLObject sentence)` Removes all existentials by replacing them with Skolem constants or Skolem sentences.
`static SubLObject`	`first_conjunction(SubLObject sentences)` Returns the first conjunction in the list SENTENCES.
`static SubLObject`	`first_disjunction(SubLObject sentences)` Returns the first disjunction in the list SENTENCES.
`static SubLObject`	`forbid_quantified_sequence_variablesP()`
`static SubLObject`	`force_into_cnf(SubLObject sentence)` Assumes that SENTENCE is a subset of CNF (either in cnf, a disjunction, or a literal) and returns a version of SENTENCE that is in strict CNF form.
`static SubLObject`	`force_into_dnf(SubLObject sentence)` Assumes that SENTENCE is a subset of DNF (either in dnf, a conjunction, or a literal) and returns a version of SENTENCE that is in strict DNF form.
`static SubLObject`	`init_clausifier_file()`
`void`	`initializeVariables()` Initializes all global variables and private internal variables for constants defined in the file.
`static SubLObject`	`leave_skolem_constants_aloneP()`
`static SubLObject`	`make_skolem_fn_fn(SubLObject var, SubLObject dependent_term_vars, SubLObject quant, SubLObject num, SubLObject dependent_sequence_var)`
`static SubLObject`	`negate_atomic(SubLObject sentence)`
`static SubLObject`	`negate_conjunction(SubLObject conjunction)` Assumes that CONJUNCTION is a conjunction.
`static SubLObject`	`negate_formula(SubLObject sentence)` Negates SENTENCE by using the following transformations: #$True becomes #$False #$False becomes #$True (#$and ) becomes (#$or (#$not ) (#$not )) (#$or ) becomes (#$and (#$not ) (#$not )) (#$not ) becomes , but is recursively simplified (#$forAll ?X ) becomes (#$thereExists ?X (#$not )) (#$thereExists ?X ) becomes (#$forAll ?X (#$not )) (#$thereExistAtLeast NUM ?X ) becomes (#$thereExistAtMost (- NUM 1) ?X (#$not )) (#$thereExistAtMost NUM ?X ) becomes (#$thereExistAtLeast (+ NUM 1) ?X (#$not )) (#$thereExistExactly NUM ?X ) becomes (#$or (#$thereExistAtLeast (+ NUM 1) ?X ) (#$thereExistAtMost (- NUM 1) ?X ) Any sentence not meeting any of the above criteria is negated by simply wrapping a #$not around it.
`static SubLObject`	`negation_in(SubLObject sentence)` Moves a negation inwards by the following transformations: 1.
`static SubLObject`	`npackage_cnf_clause(SubLObject clause)` A destructive version of @xref package-cnf-clause.
`static SubLObject`	`npackage_xnf_clause(SubLObject clause)` A destructive version of @xref package-xnf-clause.
`static SubLObject`	`package_xnf_clause(SubLObject clause)`
`static SubLObject`	`recursively_standardize_variables(SubLObject sentence)` Renames all quantified variables into a canonical order, with the innermost variables having smaller indices.
`static SubLObject`	`remember_variable_rename(SubLObject old_var, SubLObject new_var)` Remembers which variables are being renamed, and what their new names are.
`void`	`runTopLevelForms()` Runs all top-level forms in order.
`static SubLObject`	`setup_clausifier_file()`
`static SubLObject`	`skolemize_atomic_sentence(SubLObject sentence, SubLObject quantifier_info_list)`
`static SubLObject`	`skolemize_variable(SubLObject sentence, SubLObject curr_quant, SubLObject curr_num, SubLObject curr_var, SubLObject curr_free_term_vars, SubLObject curr_free_sequence_vars, SubLObject quantifier_info_list_in_scope)`
`static SubLObject`	`standardize_variables(SubLObject sentence)` Renames all variables into a canonical order, with the innermost variables having smaller indices.
`static SubLObject`	`universals_out(SubLObject sentence)` removes all #$forAll statements from SENTENCE, unless they are inside an atomic sentence.

Methods inherited from class com.cyc.tool.subl.util.SubLTranslatedFile
`extractFunctionNamed`

Methods inherited from class com.cyc.tool.subl.util.SubLTrampolineFile
`checkType, enforceType, extractBinaryFunc, extractCount, extractEnd, extractEndUsingSize, extractPackage, extractStart, extractUnaryFunc, main`

Methods inherited from class java.lang.Object
`equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

me

public static final SubLFile me

myName

public static final java.lang.String myName

See Also:: Constant Field Values

$canonical_variable_name_stem$

public static SubLSymbol $canonical_variable_name_stem$

used for standardizing EL variables in the canonicalizer

$use_cnf_cacheP$

public static SubLSymbol $use_cnf_cacheP$

Whether to cache the function that converts EL sentences to CNF clausal form

$str0$el_var

public static final SubLString $str0$el_var

$kw1$ERROR

public static final SubLSymbol $kw1$ERROR

$kw2$UNINITIALIZED

public static final SubLSymbol $kw2$UNINITIALIZED

$sym3$DO_IMPLICATIONS_RECURSIVE

public static final SubLSymbol $sym3$DO_IMPLICATIONS_RECURSIVE

$sym4$DO_NEGATIONS_DESTRUCTIVE

public static final SubLSymbol $sym4$DO_NEGATIONS_DESTRUCTIVE

$kw5$HELLO_YOU_SILLY_COMPILER

public static final SubLSymbol $kw5$HELLO_YOU_SILLY_COMPILER

$const6$True

public static final SubLObject $const6$True

$const7$False

public static final SubLObject $const7$False

$kw8$REGULARIZE

public static final SubLSymbol $kw8$REGULARIZE

$str9$_s_is_not_a_quantified_sentence

public static final SubLString $str9$_s_is_not_a_quantified_sentence

$sym10$NEGATE_NEGATION

public static final SubLSymbol $sym10$NEGATE_NEGATION

$sym11$NEGATE_FORMULA

public static final SubLSymbol $sym11$NEGATE_FORMULA

$const12$DifferenceFn

public static final SubLObject $const12$DifferenceFn

$str13$_s_contained_the_invalid_bound__D

public static final SubLString $str13$_s_contained_the_invalid_bound__D

$const14$PlusFn

public static final SubLObject $const14$PlusFn

$sym15$EL_FORMULA_P

public static final SubLSymbol $sym15$EL_FORMULA_P

$int16$32

public static final SubLInteger $int16$32

$sym17$CYC_VAR_

public static final SubLSymbol $sym17$CYC_VAR_

$const18$Quote

public static final SubLObject $const18$Quote

$sym19$RECURSIVELY_STANDARDIZE_VARIABLES

public static final SubLSymbol $sym19$RECURSIVELY_STANDARDIZE_VARIABLES

$sym20$EL_UNIQUIFY_STANDARDIZE

public static final SubLSymbol $sym20$EL_UNIQUIFY_STANDARDIZE

$sym21$EL_VAR_WITHOUT_QUOTE

public static final SubLSymbol $sym21$EL_VAR_WITHOUT_QUOTE

$kw22$IGNORE

public static final SubLSymbol $kw22$IGNORE

$str23$_

public static final SubLString $str23$_

$sym24$CYC_CONST_GENERAL_EXISTENTIAL_OPERATOR_P

public static final SubLSymbol $sym24$CYC_CONST_GENERAL_EXISTENTIAL_OPERATOR_P

$kw25$TOO_MANY_SEQUENCE_VARS_IN_SKOLEM_SCOPE

public static final SubLSymbol $kw25$TOO_MANY_SEQUENCE_VARS_IN_SKOLEM_SCOPE

$kw26$AMBIGUOUS_VAR_TYPE_IN_SKOLEM_SCOPE

public static final SubLSymbol $kw26$AMBIGUOUS_VAR_TYPE_IN_SKOLEM_SCOPE

$kw27$QUANTIFIED_SEQUENCE_VARIABLE

public static final SubLSymbol $kw27$QUANTIFIED_SEQUENCE_VARIABLE

$sym28$EXISTENTIALS_OUT_INT

public static final SubLSymbol $sym28$EXISTENTIALS_OUT_INT

$str29$Unexpected_sentence_type_in_exist

public static final SubLString $str29$Unexpected_sentence_type_in_exist

$const30$forAll

public static final SubLObject $const30$forAll

$kw31$NEITHER

public static final SubLSymbol $kw31$NEITHER

$kw32$TERM

public static final SubLSymbol $kw32$TERM

$kw33$SEQ

public static final SubLSymbol $kw33$SEQ

$kw34$BOTH

public static final SubLSymbol $kw34$BOTH

$kw35$UNDETERMINED

public static final SubLSymbol $kw35$UNDETERMINED

$str36$Skolemizer_failed_to_classify_var

public static final SubLString $str36$Skolemizer_failed_to_classify_var

$str37$skolem_constants_not_yet_supporte

public static final SubLString $str37$skolem_constants_not_yet_supporte

$const38$thereExists

public static final SubLObject $const38$thereExists

$const39$SkolemFunctionFn

public static final SubLObject $const39$SkolemFunctionFn

$str40$make_skolem_fn_fn_doesn_t_know_ho

public static final SubLString $str40$make_skolem_fn_fn_doesn_t_know_ho

$kw41$ASSERT_ONLY

public static final SubLSymbol $kw41$ASSERT_ONLY

$str42$Unexpected_value_for__forbid_quan

public static final SubLString $str42$Unexpected_value_for__forbid_quan

$sym43$UNIVERSALS_OUT

public static final SubLSymbol $sym43$UNIVERSALS_OUT

$str44$Got_the_unexpected_sentence__S_in

public static final SubLString $str44$Got_the_unexpected_sentence__S_in

$sym45$DISJUNCTIONS_IN

public static final SubLSymbol $sym45$DISJUNCTIONS_IN

$str46$Got_the_unexpected_sentence__S_in

public static final SubLString $str46$Got_the_unexpected_sentence__S_in

$sym47$EL_CONJUNCTION_P

public static final SubLSymbol $sym47$EL_CONJUNCTION_P

$kw48$BAD_EXPONENTIAL_DISJUNCTION

public static final SubLSymbol $kw48$BAD_EXPONENTIAL_DISJUNCTION

$int49$200000

public static final SubLInteger $int49$200000

$sym50$FORMULA_ARITY

public static final SubLSymbol $sym50$FORMULA_ARITY

$str51$_s_is_not_a_conjunction__so_it_is

public static final SubLString $str51$_s_is_not_a_conjunction__so_it_is

$str52$_s_is_not_a_disjunctionsoS_is

public static final SubLString $str52$_s_is_not_a_disjunction__so__S_is

$sym53$CONJUNCTIONS_IN

public static final SubLSymbol $sym53$CONJUNCTIONS_IN

$str54$Got_the_unexpected_formula__S_in_

public static final SubLString $str54$Got_the_unexpected_formula__S_in_

$sym55$EL_DISJUNCTION_P

public static final SubLSymbol $sym55$EL_DISJUNCTION_P

$kw56$BAD_EXPONENTIAL_CONJUNCTION

public static final SubLSymbol $kw56$BAD_EXPONENTIAL_CONJUNCTION

$str57$_s_is_not_a_disjunction__so_it_is

public static final SubLString $str57$_s_is_not_a_disjunction__so_it_is

$str58$_s_is_not_a_conjunctionsoS_is

public static final SubLString $str58$_s_is_not_a_conjunction__so__S_is

$sym59$PACKAGE_XNF_CLAUSE

public static final SubLSymbol $sym59$PACKAGE_XNF_CLAUSE

$sym60$FORMULA_ARG1

public static final SubLSymbol $sym60$FORMULA_ARG1

$sym61$EL_VAR_

public static final SubLSymbol $sym61$EL_VAR_

$sym62$LEADING_UNIVERSAL_VARIABLES_1

public static final SubLSymbol $sym62$LEADING_UNIVERSAL_VARIABLES_1

$sym63$STRING_

public static final SubLSymbol $sym63$STRING_

$sym64$STR

public static final SubLSymbol $sym64$STR

$const65$and

public static final SubLObject $const65$and

$kw66$CNF

public static final SubLSymbol $kw66$CNF

$kw67$DNF

public static final SubLSymbol $kw67$DNF

$sym68$CACHED_CNF_CLAUSAL_FORM

public static final SubLSymbol $sym68$CACHED_CNF_CLAUSAL_FORM

$sym69$_CACHED_CNF_CLAUSAL_FORM_CACHING_STATE_

public static final SubLSymbol $sym69$_CACHED_CNF_CLAUSAL_FORM_CACHING_STATE_

$int70$48

public static final SubLInteger $int70$48

$kw71$_MEMOIZED_ITEM_NOT_FOUND_

public static final SubLSymbol $kw71$_MEMOIZED_ITEM_NOT_FOUND_

Method Detail

do_implications

public static final SubLObject do_implications(SubLObject sentence)

do_implications_recursive

public static final SubLObject do_implications_recursive(SubLObject sentence)

Removes all implications and equivalences from SENTENCE, returning a logically equivalent sentence. Converts (#$implies ) to (#$or (#$not ) ). Does not simplify nested negations, disjunctions, or conjunctions.

do_negations_destructive

public static final SubLObject do_negations_destructive(SubLObject sentence)

A destructive version of @xref do-negations.

negate_formula

public static final SubLObject negate_formula(SubLObject sentence)

Negates SENTENCE by using the following transformations:

#$True becomes #$False
#$False becomes #$True
(#$and ) becomes (#$or (#$not ) (#$not ))
(#$or ) becomes (#$and (#$not ) (#$not ))
(#$not ) becomes , but is recursively simplified
(#$forAll ?X ) becomes (#$thereExists ?X (#$not ))
(#$thereExists ?X ) becomes (#$forAll ?X (#$not ))
(#$thereExistAtLeast NUM ?X ) becomes (#$thereExistAtMost (- NUM 1) ?X (#$not ))
(#$thereExistAtMost NUM ?X ) becomes (#$thereExistAtLeast (+ NUM 1) ?X (#$not ))
(#$thereExistExactly NUM ?X ) becomes (#$or (#$thereExistAtLeast (+ NUM 1) ?X ) (#$thereExistAtMost (- NUM 1) ?X )

Any sentence not meeting any of the above criteria is negated by simply wrapping a #$not around it.

negation_in

public static final SubLObject negation_in(SubLObject sentence)

Moves a negation inwards by the following transformations: 1. (#$not #$True) becomes #$False 2. (#$not #$False) becomes #$True 3. (#$not (#$and )) becomes (#$or (#$not ) (#$not )) 4. (#$not (#$or )) becomes (#$and (#$not ) (#$not )) 5. (#$not (#$not )) becomes , but is recursively simplified 6. (#$not (#$forAll ?X )) becomes (#$thereExists ?X (#$not )) 7. (#$not (#$thereExists ?X )) becomes (#$forAll ?X (#$not )) 8. (#$not (#$thereExistAtLeast NUM ?X )) becomes (#$thereExistAtMost (- NUM 1) ?X (#$not )) 9. (#$not (#$thereExistAtMost NUM ?X )) becomes (#$thereExistAtLeast (+ NUM 1) ?X (#$not )) 10. (#$not (#$thereExistExactly NUM ?X )) becomes (#$or (#$thereExistAtLeast (+ NUM 1) ?X ) (#$thereExistAtMost (- NUM 1) ?X ) Note that negated implications or other forms are not simplified. If this function does make a simplification, it is guaranteed to return something that is not a negation. If you pass a sentence that is not a negation, it will return that sentence without any changes.

negate_atomic

public static final SubLObject negate_atomic(SubLObject sentence)

Returns:: EL sentence; negation of SENTENCE. Assumes that SENTENCE is atomic and does no simplification.

negate_conjunction

public static final SubLObject negate_conjunction(SubLObject conjunction)

Assumes that CONJUNCTION is a conjunction. Moves negations inwards by the following transformation: (#$and ) becomes (#$or (#$not ) (#$not ))

czer_explicitify_implicit_quantifiers

public static final SubLObject czer_explicitify_implicit_quantifiers(SubLObject sentence)

czer_explicitify_implicit_universal_quantifiers

public static final SubLObject czer_explicitify_implicit_universal_quantifiers(SubLObject sentence)

Wraps SENTENCE in #$forAll statements (if needed) to quantify all the free variables within SENTENCE. Should appear within a binding of *newly-introduced-universals*

See Also:: explicitify-implicit-universal-quantifiers

assume_free_vars_are_existentially_boundP

public static final SubLObject assume_free_vars_are_existentially_boundP()

standardize_variables

public static final SubLObject standardize_variables(SubLObject sentence)

Renames all variables into a canonical order, with the innermost variables having smaller indices. Assumes that all universal quantification is explicit. Assumes that the EL variable namespace is bound.

remember_variable_rename

public static final SubLObject remember_variable_rename(SubLObject old_var,
                                                        SubLObject new_var)

Remembers which variables are being renamed, and what their new names are. Assumes that *standardize-variables-memory* is bound.

recursively_standardize_variables

public static final SubLObject recursively_standardize_variables(SubLObject sentence)

Renames all quantified variables into a canonical order, with the innermost variables having smaller indices. Variables at the same depth are ordered from left to right. Assumes that *standardize-variables-memory* is bound. Also assumes that implications and other weird logical operators have been removed.

el_var_without_quote

public static final SubLObject el_var_without_quote(SubLObject var)

el_uniquify_standardize

public static final SubLObject el_uniquify_standardize(SubLObject var)

el_uniquify

public static final SubLObject el_uniquify(SubLObject var)

Assumes that *el-symbol-suffix-table* is bound.

existentials_out

public static final SubLObject existentials_out(SubLObject sentence)

Removes all existentials by replacing them with Skolem constants or Skolem sentences.

existentials_out_int

public static final SubLObject existentials_out_int(SubLObject sentence)

Removes all existentials by replacing them with Skolem constants or Skolem sentences. Keeps a list of the quantifiers whose scope we are within to determine the free variables in the Skolem sentences. Assumes that *quantifier-info-list* is bound.

skolemize_atomic_sentence

public static final SubLObject skolemize_atomic_sentence(SubLObject sentence,
                                                         SubLObject quantifier_info_list)

drop_all_existentialsP

public static final SubLObject drop_all_existentialsP()

Returns:: booleanp; whether the clausifier should, when canonicalizing existentials, simply drop them (like it does by default during asks)?

forbid_quantified_sequence_variablesP

public static final SubLObject forbid_quantified_sequence_variablesP()

skolemize_variable

public static final SubLObject skolemize_variable(SubLObject sentence,
                                                  SubLObject curr_quant,
                                                  SubLObject curr_num,
                                                  SubLObject curr_var,
                                                  SubLObject curr_free_term_vars,
                                                  SubLObject curr_free_sequence_vars,
                                                  SubLObject quantifier_info_list_in_scope)

leave_skolem_constants_aloneP

public static final SubLObject leave_skolem_constants_aloneP()

make_skolem_fn_fn

public static final SubLObject make_skolem_fn_fn(SubLObject var,
                                                 SubLObject dependent_term_vars,
                                                 SubLObject quant,
                                                 SubLObject num,
                                                 SubLObject dependent_sequence_var)

Parameters:: DEPENDENT-SEQUENCE-VAR; - nil or cycl-variable-p

determine_skolem_var_status

public static final SubLObject determine_skolem_var_status(SubLObject var,
                                                           SubLObject subsent_free_term_vars,
                                                           SubLObject free_term_vars_in_scope,
                                                           SubLObject subsent_free_seqvars,
                                                           SubLObject free_seqvars_in_scope)

Parameters:: VAR; - the universally scoped variable whose status we need to determine wrt an existential. Example: In a sentence of the form (forAll ?X (forAll ?Y (implies (isa ?Y Ort) (thereExists ?Z (mother ?X ?Z))))) The subsentence in consideration would be (mother ?X ?Z), its free term vars would be ?X and ?Z, and the free term vars in the scope would be ?X and ?Y. If VAR is ?X, the result would be :term. If VAR is ?Y, the result would be :term or :neither, depending on *minimal-skolem-arity?*
Returns:: keywordp; :neither, :term, :seq, :both, or :undetermined

universals_out

public static final SubLObject universals_out(SubLObject sentence)

removes all #$forAll statements from SENTENCE, unless they are inside an atomic sentence. Assumes that the only logical operators in SENTENCE are #$forAll, #$and, #$or, and #$not, and that #$not only appears around an atomic sentence. Also assumes that the outermost #$ist's have been removed.

disjunctions_in

public static final SubLObject disjunctions_in(SubLObject sentence)

disjunctions_in_int

public static final SubLObject disjunctions_in_int(SubLObject sentence)

Moves disjunctions inwards inside SENTENCE by repeatedly applying the following transformation: (#$or (#$and )) becomes (#$and (#$or ) (#$or )). (#$or (#$and )) becomes (#$and (#$or ) (#$or )). Assumes that the only logical operators in SENTENCE are #$and, #$or, and #$not, and that #$not only encloses atomic sentences. The order is scrambled when the disjunctions are pushed inwards.

first_conjunction

public static final SubLObject first_conjunction(SubLObject sentences)

Returns the first conjunction in the list SENTENCES.

bad_exponential_disjunctionP

public static final SubLObject bad_exponential_disjunctionP(SubLObject sentence)

Returns:: booleanp; whether SENTENCE is too explosive to be put into CNF using the straightforward algorithm.

bad_exponential_sentenceP

public static final SubLObject bad_exponential_sentenceP(SubLObject sentence,
                                                         SubLObject arg_test_func)

force_into_cnf

public static final SubLObject force_into_cnf(SubLObject sentence)

Assumes that SENTENCE is a subset of CNF (either in cnf, a disjunction, or a literal) and returns a version of SENTENCE that is in strict CNF form. For example, (#$genls #$Dog #$Mammal) would be forced into (#$and (#or (#$genls #$Dog #$Mammal))). Also, it scrambles the order of the arguments inside the conjunctions and disjunctions.

cnf_operators_out

public static final SubLObject cnf_operators_out(SubLObject sentence)

Parameters:: sentence - EL sentence; a conjunction of possibly disjoined literals.
Returns:: clauses; a list of cnf-clauses, each of which is a pair: ( ( ) ...) Removes #$and, #$or and #$not while translating a sentence of the form (#$and (#$or (#$not ) ...) (#$or (#$not ) (#$not ) ...) ...) into ( (( ...) ( ...)) (( ...) ( ...)) ... )

npackage_cnf_clause

public static final SubLObject npackage_cnf_clause(SubLObject clause)

A destructive version of @xref package-cnf-clause.

conjunctions_in

public static final SubLObject conjunctions_in(SubLObject sentence)

conjunctions_in_int

public static final SubLObject conjunctions_in_int(SubLObject sentence)

Moves conjunctions inwards inside SENTENCE by repeatedly applying the following transformation: (#$and (#$or )) becomes (#$or (#$and ) (#$and )). (#$and (#$or )) becomes (#$or (#$and ) (#$and )). Assumes that the only logical operators in SENTENCE are #$and, #$or, and #$not, and that #$not only encloses atomic sentences. The order is scrambled when the conjunctions are pushed inwards.

first_disjunction

public static final SubLObject first_disjunction(SubLObject sentences)

Returns the first disjunction in the list SENTENCES.

bad_exponential_conjunctionP

public static final SubLObject bad_exponential_conjunctionP(SubLObject sentence)

Returns:: booleanp; whether SENTENCE is too explosive to be put into DNF using the straightforward algorithm.

force_into_dnf

public static final SubLObject force_into_dnf(SubLObject sentence)

Assumes that SENTENCE is a subset of DNF (either in dnf, a conjunction, or a literal) and returns a version of SENTENCE that is in strict DNF form. For example, (#$genls #$Dog #$Mammal) would be forced into (#$or (#$and (#$genls #$Dog #$Mammal))). Also, it scrambles the order of the arguments inside the disjunctions and conjunctions.

dnf_operators_out

public static final SubLObject dnf_operators_out(SubLObject sentence)

Parameters:: sentence - EL sentence; a disjunction of possibly conjoined literals.
Returns:: clauses; a list of dnf-clauses, each of which is a pair: ( ( ) ...) Removes #$or, #$and and #$not while translating a sentence of the form (#$or (#$and (#$not ) ...) (#$and (#$not ) (#$not ) ...) ...) into ( (( ...) ( ...)) (( ...) ( ...)) ... )

el_xnf

public static final SubLObject el_xnf(SubLObject sentence,
                                      SubLObject mt)

Transforms an EL sentence so that it is ready to be put into either CNF or DNF form. At the end of this step, the only operators in SENTENCE will be #$and, #$or, and #$not, and #$not will only enclose atomic sentences. Most transformations are syntactic except for the precanonicalizations.

Returns:: 0 EL sentence Assumes the EL var namespace is bound.

el_xnf_int

public static final SubLObject el_xnf_int(SubLObject sentence,
                                          SubLObject mt)

package_xnf_clause

public static final SubLObject package_xnf_clause(SubLObject clause)

Parameters:: clause - list; a list of literals. Goes through CLAUSE looking for negated atomic sentences. It puts them into and puts the rest into .
Returns:: list; ( )

npackage_xnf_clause

public static final SubLObject npackage_xnf_clause(SubLObject clause)

A destructive version of @xref package-xnf-clause.

canon_fast_gafP

public static final SubLObject canon_fast_gafP(SubLObject sentence,
                                               SubLObject mt)

el_cnf

public static final SubLObject el_cnf(SubLObject sentence,
                                      SubLObject mt)

Constructively transforms an EL sentence into conjunctive normal form. Returns a well-formed EL sentence, or NIL if there was an error. Semantic checks are performed only at the beginning and end - all internal processing is purely syntactic.

Returns:: 0 EL sentence

el_cnf_destructive

public static final SubLObject el_cnf_destructive(SubLObject sentence,
                                                  SubLObject mt)

Destructively transforms an EL sentence into conjunctive normal form. Returns a well-formed EL sentence, or NIL if there was an error. Semantic checks are performed only at the beginning and end - all internal processing is purely syntactic.

Returns:: 0 EL sentence Assumes the EL variable namespace is bound.

el_cnf_int

public static final SubLObject el_cnf_int(SubLObject sentence,
                                          SubLObject mt,
                                          SubLObject destructiveP)

Assumes the EL variable namespace is bound.

el_dnf_destructive

public static final SubLObject el_dnf_destructive(SubLObject sentence,
                                                  SubLObject mt)

Destructively transforms an EL sentence into disjunctive normal form. Returns a well-formed EL sentence, or NIL if there was an error. Semantic checks are performed only at the beginning and end - all internal processing is purely syntactic.

Returns:: 0 EL sentence Assumes the EL variable namespace is bound.

el_dnf_int

public static final SubLObject el_dnf_int(SubLObject sentence,
                                          SubLObject mt,
                                          SubLObject destructiveP)

Assumes the EL variable namespace is bound.

cnf_clausal_form

public static final SubLObject cnf_clausal_form(SubLObject sentence,
                                                SubLObject mt)

Returns:: 0 EL sentence; the CNF form of the EL sentence SENTENCE.

clear_cached_cnf_clausal_form

public static final SubLObject clear_cached_cnf_clausal_form()

cnf_clausal_form_int

public static final SubLObject cnf_clausal_form_int(SubLObject sentence,
                                                    SubLObject mt)

declare_clausifier_file

public static final SubLObject declare_clausifier_file()

init_clausifier_file

public static final SubLObject init_clausifier_file()

setup_clausifier_file

public static final SubLObject setup_clausifier_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.

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

com.cyc.cycjava.cycl Class clausifier

me

myName

$canonical_variable_name_stem$

$use_cnf_cacheP$

$str0$el_var

$kw1$ERROR

$kw2$UNINITIALIZED

$sym3$DO_IMPLICATIONS_RECURSIVE

$sym4$DO_NEGATIONS_DESTRUCTIVE

$kw5$HELLO_YOU_SILLY_COMPILER

$const6$True

$const7$False

$kw8$REGULARIZE

$str9$_s_is_not_a_quantified_sentence

$sym10$NEGATE_NEGATION

$sym11$NEGATE_FORMULA

$const12$DifferenceFn

$str13$_s_contained_the_invalid_bound__D

$const14$PlusFn

$sym15$EL_FORMULA_P

$int16$32

$sym17$CYC_VAR_

$const18$Quote

$sym19$RECURSIVELY_STANDARDIZE_VARIABLES

$sym20$EL_UNIQUIFY_STANDARDIZE

$sym21$EL_VAR_WITHOUT_QUOTE

$kw22$IGNORE

$str23$_

$sym24$CYC_CONST_GENERAL_EXISTENTIAL_OPERATOR_P

$kw25$TOO_MANY_SEQUENCE_VARS_IN_SKOLEM_SCOPE

$kw26$AMBIGUOUS_VAR_TYPE_IN_SKOLEM_SCOPE

$kw27$QUANTIFIED_SEQUENCE_VARIABLE

$sym28$EXISTENTIALS_OUT_INT

$str29$Unexpected_sentence_type_in_exist

$const30$forAll

$kw31$NEITHER

$kw32$TERM

$kw33$SEQ

$kw34$BOTH

$kw35$UNDETERMINED

$str36$Skolemizer_failed_to_classify_var

$str37$skolem_constants_not_yet_supporte

$const38$thereExists

$const39$SkolemFunctionFn

$str40$make_skolem_fn_fn_doesn_t_know_ho

$kw41$ASSERT_ONLY

$str42$Unexpected_value_for__forbid_quan

$sym43$UNIVERSALS_OUT

$str44$Got_the_unexpected_sentence__S_in

$sym45$DISJUNCTIONS_IN

$str46$Got_the_unexpected_sentence__S_in

$sym47$EL_CONJUNCTION_P

$kw48$BAD_EXPONENTIAL_DISJUNCTION

$int49$200000

$sym50$FORMULA_ARITY

$str51$_s_is_not_a_conjunction__so_it_is

$str52$_s_is_not_a_disjunction__so__S_is

$sym53$CONJUNCTIONS_IN

$str54$Got_the_unexpected_formula__S_in_

$sym55$EL_DISJUNCTION_P

$kw56$BAD_EXPONENTIAL_CONJUNCTION

$str57$_s_is_not_a_disjunction__so_it_is

$str58$_s_is_not_a_conjunction__so__S_is

$sym59$PACKAGE_XNF_CLAUSE

$sym60$FORMULA_ARG1

$sym61$EL_VAR_

$sym62$LEADING_UNIVERSAL_VARIABLES_1

$sym63$STRING_

$sym64$STR

$const65$and

$kw66$CNF

$kw67$DNF

$sym68$CACHED_CNF_CLAUSAL_FORM

$sym69$_CACHED_CNF_CLAUSAL_FORM_CACHING_STATE_

$int70$48

$kw71$_MEMOIZED_ITEM_NOT_FOUND_

do_implications

do_implications_recursive

do_negations_destructive

com.cyc.cycjava.cycl
Class clausifier

$str52$_s_is_not_a_disjunctionsoS_is

$str58$_s_is_not_a_conjunctionsoS_is