Uses of Class
com.articulate.sigma.Formula

Packages that use Formula

Package	Description
com.articulate.sigma	Provides classes for the Sigma knowledge engineering environment version developed at Articulate Software Inc.
com.articulate.sigma.nlg	Provides classes for natural language generation in the Sigma knowledge engineering environment version developed at Articulate Software Inc.
com.articulate.sigma.parsing
com.articulate.sigma.tp
com.articulate.sigma.trans	Provides classes for translation to other logical languages in the Sigma knowledge engineering environment version developed at Articulate Software Inc.
com.articulate.sigma.wordNet	Provides classes for handling Wordnets.

Uses of Formula in com.articulate.sigma

Fields in com.articulate.sigma with type parameters of type Formula

Modifier and Type	Field	Description
List<Formula>	Formula.args
static Map<String,Formula>	KB.axiomKey	maps TPTP axiom IDs to SUMO formulas
Map<String,Formula>	KB.formulaMap	A Map of all the Formula objects in the KB.
Map<String,Formula>	KIF.formulaMap	A HashMap of String keys representing the formula, and Formula values.
Map<Integer,Formula>	KIF.formulasOrdered
List<Formula>	Derivation.parents

Methods in com.articulate.sigma that return Formula

Modifier and Type	Method	Description
Formula	FormulaPreprocessor.addTypeRestrictions(Formula form, KB kb)	Add clauses for every variable in the antecedent to restrict its type to the type restrictions defined on every relation in which it appears.
Formula	Formula.append(Formula f)	Returns the LISP 'append' of the formulas Note that this operation has no side effect on the Formula.
Formula	Prenexifier.binarizeConnectives(Formula f)
Formula	Formula.carAsFormula()	Returns the LISP 'car' of the formula as a new Formula, if possible, else returns null.
Formula	Formula.cddrAsFormula()	Returns the LISP 'cddr' of the formula as a new Formula, if possible, else returns null.
Formula	Formula.cdrAsFormula()	Returns the LISP 'cdr' of the formula as a new Formula, if possible, else returns null.
Formula	Clausifier.clausify()	This method converts the SUO-KIF Formula to a version of clausal (resolution, conjunctive normal) form with Skolem functions, following the procedure described in Logical Foundations of Artificial Intelligence, by Michael Genesereth and Nils Nilsson, 1987, pp.
static Formula	Clausifier.clausify(Formula f)	convenience method
Formula	Formula.cons(Formula f)
Formula	Formula.cons(String obj)	Returns a new Formula which is the result of 'consing' a String into this Formula, similar to the LISP procedure of the same name.
Formula	Formula.copy()	Copy the Formula.
static Formula	Formula.createComment(String input)	the textual version of the formula
Formula	Formula.deepCopy()
Formula	Formula.getArgument(int argnum)	Return the numbered argument of the given formula.
Formula	KB.getFormulaByKey(String key)	An accessor providing a Formula
static Formula	KB.literalListToFormula(List<String> lit)	Converts a literal (List object) to a Formula.
Formula	Formula.negate()
Formula	Prenexifier.prenex(Formula f)
Formula	Clausifier.rename(String term2, String term1)	Replace term2 with term1
Formula	Formula.rename(String term2, String term1)	Replace term2 with term1
Formula	Formula.renameVariableArityRelations(KB kb, Map<String,String> relationMap)
static Formula	Clausifier.renameVariables(Formula f)	convenience method
static Formula	Clausifier.renameVariables(Formula f, Map topLevelVars, Map scopedRenames, Map allRenames)	convenience method
Formula	Formula.replaceQuantifierVars(String quantifier, List<String> vars)
Formula	Formula.replaceVar(String v, String term)	Replace v with term.
Formula	Clausifier.substituteVariables(Map<String,String> m)	Replace variables with a value as given by the map argument
Formula	Formula.substituteVariables(Map<String,String> m)	Replace variables with a value as given by the map argument
Formula	Clausifier.toCanonicalClausalForm()	This method converts the SUO-KIF Formula to a canonical version of clausal (resolution, conjunctive normal) form with Skolem functions, following the procedure described in Logical Foundations of Artificial Intelligence, by Michael Genesereth and Nils Nilsson, 1987, pp.
static Formula	Clausifier.toCanonicalClausalForm(Formula f)	convenience method
protected Formula	Clausifier.toCanonicalKifSpecialForm(boolean preserveSharedVariables)	This method returns a canonical version of this Formula, assumed to be a KIF "special" form, in which all internal first-order KIF formulae are replaced by their canonical versions, and all variables are renamed, in left to right depth-first order of occurrence, starting from index 1.
protected Formula	Clausifier.toOpenQueryForNegatedDualForm()	This method returns an open Formula that constitutes a KIF query expression, which is generated from the canonicalized negation of the original Formula.
static Formula	Clausifier.universalsOut(Formula f)	convenience method

Methods in com.articulate.sigma that return types with arguments of type Formula

Modifier and Type	Method	Description
List<Formula>	Formula.argumentsToArrayList(int start)	Deprecated.
List<Formula>	KB.ask(String kind, int argnum, String term)	Returns an ArrayList containing the Formulas that match the request.
List<Formula>	KB.askWithLiteral(Formula queryLit)	This method retrieves formulas by asking the query expression queryLit, and returns the results, if any, in an ArrayList.
List<Formula>	KB.askWithLiteral(List<String> queryLit)	This method retrieves Formulas by asking the query expression queryLit, and returns the results, if any, in an ArrayList.
List<Formula>	KB.askWithPredicateSubsumption(String relation, int idxArgnum, String idxTerm)	Returns an ArrayList containing the Formulae retrieved, possibly via multiple asks that recursively use relation and all of its subrelations.
List<Formula>	KB.askWithRestriction(int argnum1, String term1, int argnum2, String term2)
List<Formula>	KB.askWithTwoRestrictions(int argnum1, String term1, int argnum2, String term2, int argnum3, String term3)	Returns an ArrayList of Formulas in which the two terms provided appear in the indicated argument positions.
static List<Formula>	KB.atomsToFormulas(List<String> strings)
static Set<Formula>	KifFileChecker.CheckFormulaPreprocess(String fileName, KB kb, Formula f, int formulaStartLine, List<ErrRec> msgs)	Run FormulaPreprocessor and record errors/warnings.
static Map<String,Formula>	KB.collectSourceAxioms(KB kb, TPTP3ProofProcessor tpp)	Attempt to provide guidance on the likely cause of a contradiction by removing the axioms involved in a contradiction one-by-one and trying again.
List<Formula>	Formula.complexArgumentsToArrayList(int start)	Return all the arguments in a formula as a list, starting at the given argument.
static List<Formula>	RowVars.expandRowVars(KB kb, Formula f)	Expand row variables, keeping the information about the original source formula.
static Set<Formula>	KButilities.getAllFormulasOfTerm(KB kb, String term)	Find all formulas in which the SUMO term is involved.
List<Formula>	Derivation.getParents()	Return a list of all derived objects that are used in this derivation.
protected static Set<Formula>	PredVarInst.handleDoubles(KB kb)	A bit of a hack to produce the statements that would result from the only two axioms in SUMO with two predicate variables
List<Formula>	KB.instancesOf(String term)	Determine whether a particular term is an immediate instance, which has a statement of the form (instance term otherTerm).
static Set<Formula>	PredVarInst.instantiatePredVars(Formula input, KB kb)
List<Formula>	KIF.lexicalOrder()	Return an ArrayList of Formula in the same lexical order as their source file
List<Formula>	KB.merge(KIF kif, String pathname)	Merges a KIF object containing a single formula into the current KB.
Set<Formula>	FormulaPreprocessor.preProcess(Formula form, boolean isQuery, KB kb)	Pre-process a formula before sending it to the theorem prover.
static List<Formula>	Diagnostics.quantifierNotInBody(KB kb)	Find cases where a variable appears in a quantifier list, but not in the body of the quantified expression.
static List<Formula>	Diagnostics.quantifierNotInBody(KB kb, String fname)	Find cases where a variable appears in a quantifier list, but not in the body of the quantified expression.
static List<Formula>	TaxoModel.removeCached(List<Formula> forms)	Remove any cached formulas from a list.
protected List<Formula>	FormulaPreprocessor.replacePredVarsAndRowVars(Formula form, KB kb, boolean addHoldsPrefix)	Tries to successively instantiate predicate variables and then expand row variables in this Formula, looping until no new Formulae are generated.
List<Formula>	Clausifier.separateConjunctions()	Turn a conjunction into an ArrayList of separate statements
static List<Formula>	Clausifier.separateConjunctions(Formula f)	convenience method
static List<Formula>	KButilities.termIntersection(KB kb, String term1, String term2)	Get all formulas that contain both terms.
static List<Formula>	Diagnostics.unquantsInConseq(KB kb)

Methods in com.articulate.sigma with parameters of type Formula

Modifier and Type	Method	Description
protected static Map<String,Set<String>>	PredVarInst.addExplicitTypes(KB kb, Formula input, Map<String,Set<String>> types)	There are two type conditions: one type condition is extracted from domain expression; second type condition is specifically defined in the antecedent of a rule with an instance or subclass expression
Formula	FormulaPreprocessor.addTypeRestrictions(Formula form, KB kb)	Add clauses for every variable in the antecedent to restrict its type to the type restrictions defined on every relation in which it appears.
static String	FormulaUtil.antecedent(Formula f)	Get the antecedent of an implication.
Formula	Formula.append(Formula f)	Returns the LISP 'append' of the formulas Note that this operation has no side effect on the Formula.
List<Formula>	KB.askWithLiteral(Formula queryLit)	This method retrieves formulas by asking the query expression queryLit, and returns the results, if any, in an ArrayList.
Formula	Prenexifier.binarizeConnectives(Formula f)
static void	KifFileChecker.CheckExistentialInAntecedent(String fileName, Formula f, String formulaText, int formulaStartLine, List<ErrRec> msgs)	Check for existential quantifiers in antecedents (illegal).
static Set<Formula>	KifFileChecker.CheckFormulaPreprocess(String fileName, KB kb, Formula f, int formulaStartLine, List<ErrRec> msgs)	Run FormulaPreprocessor and record errors/warnings.
static void	KifFileChecker.CheckIsValidFormula(String fileName, Formula f, int formulaStartLine, KB kb, String formulaText, List<ErrRec> msgs)	Check if the formula is structurally valid in the KB.
static void	KifFileChecker.CheckOrphanVars(String fileName, Formula f, String formulaText, int formulaStartLine, List<ErrRec> msgs)	Check for disconnected variable groups
static void	KifFileChecker.CheckQuantifiedVariableNotInStatement(String fileName, Formula f, String formulaText, int formulaStartLine, List<ErrRec> msgs)	Check for quantified variables that do not appear in the statement body.
static void	KifFileChecker.CheckSingleUseVariables(String fileName, Formula f, String formulaText, int formulaStartLine, List<ErrRec> msgs)	Check for variables that appear only once in a formula.
static void	KifFileChecker.CheckSUMOtoTFAformErrors(String fileName, KB kb, Formula f, int formulaStartLine, Set<Formula> processed, List<ErrRec> msgs)	Correct invocation of SUMO→TFA translation errors.
static void	KifFileChecker.CheckTermsBelowEntity(String fileName, Formula f, int formulaStartLine, String formulaText, KB kb, Set<String> localIndividuals, Set<String> localSubclasses, List<ErrRec> msgs)	Check that all terms are below Entity in the KB hierarchy.
static void	KifFileChecker.CheckUnquantInConsequent(String fileName, Formula f, String formulaText, int formulaStartLine, List<ErrRec> msgs)	Check for unquantified variables appearing in the consequent of implications.
static Formula	Clausifier.clausify(Formula f)	convenience method
void	Formula.collectQuantifiedUnquantifiedVariablesRecurse(Formula f, Map<String,Boolean> varFlag, Set<String> unquantifiedVariables, Set<String> quantifiedVariables)	Collect quantified and unquantified variables recursively
Map<String,Set<String>>	FormulaPreprocessor.computeVariableTypes(Formula form, KB kb)	This method returns a HashMap that maps each String variable in this the names of types (classes) of which the variable must be an instance or the names of types of which the variable must be a subclass.
Formula	Formula.cons(Formula f)
static String	FormulaUtil.consequent(Formula f)	Get the consequent of an implication.
static String	Editor.createFormPage(KB kb, String term, Formula f)	Create an HTML form for editing facts about a term.
boolean	Formula.deepEquals(Formula f)	Test if the contents of the formula are equal to the argument.
static boolean	Diagnostics.existentialInAntecedent(Formula f)
static List<Formula>	RowVars.expandRowVars(KB kb, Formula f)	Expand row variables, keeping the information about the original source formula.
static Set<String>	Clausifier.extractVariables(Formula f)	Extract all variables in a list
Map<String,Set<String>>	FormulaPreprocessor.findAllTypeRestrictions(Formula form, KB kb)
Map<String,Set<String>>	FormulaPreprocessor.findExplicitTypes(KB kb, Formula form)	Collect variable names and their types from instance or subclass expressions.
void	FormulaPreprocessor.findExplicitTypesClasses(KB kb, Formula form, Map<String,Set<String>> varExplicitTypes, Map<String,Set<String>> varExplicitClasses)	Collect variable names and their types from instance or subclass expressions.
Map<String,Set<String>>	FormulaPreprocessor.findExplicitTypesClassesInAntecedent(KB kb, Formula form)	Collect the types of any variables that are specifically defined in the antecedent of a rule with an instance expression; Collect the super classes of any variables that are specifically defined in the antecedent of a rule with an subclass expression;
Map<String,Set<String>>	FormulaPreprocessor.findExplicitTypesInAntecedent(KB kb, Formula form)	Collect the types of any variables that are specifically defined in the antecedent of a rule with an instance or subclass expression.
static void	FormulaPreprocessor.findExplicitTypesRecurse(KB kb, Formula form, boolean isNegativeLiteral, Map<String,Set<String>> varExplicitTypes, Map<String,Set<String>> varExplicitClasses)	Recursively collect a variable name and its types.
static HashMap<String,HashSet<String>>	Diagnostics.findOrphanVars(Formula f)	Builds a map of variable co-occurrences in a formula
protected static Map<String,Set<String>>	PredVarInst.findPredVarTypes(Formula f, KB kb)	Get a set of all the types for predicate variables in the formula.
static Set<String>	RowVars.findRowVars(Formula f)
Map<String,Set<String>>	FormulaPreprocessor.findTypeRestrictions(Formula form, KB kb)	Find all the type restrictions on the variables in a formula, including constraints from relation argument typing as well as explicitly stated types from instance and subclass expressions.
protected static Set<String>	PredVarInst.gatherPredVarRecurse(KB kb, Formula f)	Get a set of all the predicate variables in the formula.
static Set<String>	PredVarInst.gatherPredVars(KB kb, Formula f)	Collect and return all predicate variables for the given formula
static String	FormulaUtil.getLiteralWithPredAndRowVar(String pred, Formula f)
static Map<String,Integer>	RowVars.getRowVarMaxAritiesWithOtherArgs(Map<String,Set<String>> ar, KB kb, Formula f)
static Map<String,Integer>	RowVars.getRowVarMinAritiesWithOtherArgs(Map<String,Set<String>> ar, KB kb, Formula f)
protected static Map<String,Set<String>>	RowVars.getRowVarRelations(Formula f)	Recurse through the formula looking for row variables.
static void	KifFileChecker.harvestLocalFacts(Formula f, Set<String> localIndividuals, Set<String> localSubclasses)	Recursively collect local individuals and subclasses from formulas.
static String	PredVarInst.hasCorrectArity(Formula f, KB kb)	If arity is correct, return null, otherwise, return the predicate that has its arity violated in the given formula.
static boolean	KButilities.hasCorrectTypes(KB kb, Formula f)	Checks for consistent typing in the given formula
static Set<Formula>	PredVarInst.instantiatePredVars(Formula input, KB kb)
static boolean	FormulaUtil.isDoc(Formula f)	Test whether a formula is suitable for theorem proving or if it's just a documentation statement
boolean	KB.isFunctional(Formula form)	Returns true if argument is functional expression, else returns false.
boolean	Formula.logicallyEquals(Formula f)	Tests if this is logically equal with the parameter formula.
static List<Set<VariableMapping>>	Formula.mapFormulaVariables(Formula f1, Formula f2, KB kb, Map<FormulaUtil.FormulaMatchMemoMapKey,List<Set<VariableMapping>>> memoMap)	Compares two formulae by recursively traversing its predicate structure and by building possible variable maps between the variables of the two formulae.
Formula	Prenexifier.prenex(Formula f)
Set<Formula>	FormulaPreprocessor.preProcess(Formula form, boolean isQuery, KB kb)	Pre-process a formula before sending it to the theorem prover.
static boolean	Diagnostics.quantifierNotInStatement(Formula f)
static String	FormulaUtil.removeAnswerClause(Formula f)	Factory method for the memo map
static Formula	Clausifier.renameVariables(Formula f)	convenience method
static Formula	Clausifier.renameVariables(Formula f, Map topLevelVars, Map scopedRenames, Map allRenames)	convenience method
protected List<Formula>	FormulaPreprocessor.replacePredVarsAndRowVars(Formula form, KB kb, boolean addHoldsPrefix)	Tries to successively instantiate predicate variables and then expand row variables in this Formula, looping until no new Formulae are generated.
static List<Formula>	Clausifier.separateConjunctions(Formula f)	convenience method
static Set<String>	Diagnostics.singleUseVariables(Formula f)
static Formula	Clausifier.toCanonicalClausalForm(Formula f)	convenience method
static List	Clausifier.toNegAndPosLitsWithRenameInfo(Formula f)	convenience method
static String	FormulaUtil.toProlog(Formula f)	Must check that this is a simple clause before calling!
boolean	Formula.unifyWith(Formula f)	Deprecated.
static Formula	Clausifier.universalsOut(Formula f)	convenience method
static Set<String>	Diagnostics.unquantInConsequent(Formula f)

Method parameters in com.articulate.sigma with type arguments of type Formula

Modifier and Type	Method	Description
static void	KifFileChecker.CheckSUMOtoTFAformErrors(String fileName, KB kb, Formula f, int formulaStartLine, Set<Formula> processed, List<ErrRec> msgs)	Correct invocation of SUMO→TFA translation errors.
static Set<String>	KBcache.collectArgFromFormulas(int arg, List<Formula> forms)	Get the HashSet of the given arguments from an ArrayList of Formulas.
static String	FormulaUtil.formatCollection(Collection<Formula> c)
static String	HTMLformatter.formatFormulaList(List<Formula> forms, String header, KB kb, String language, String flang, int start, int localLimit, String limitString)	Create the HTML for a section of the Sigma term browser page.
static List<List<String>>	KB.formulasToArrayLists(List<Formula> formulaList)	Converts all Formula objects in the input List to ArrayList tuples.
static List<Formula>	TaxoModel.removeCached(List<Formula> forms)	Remove any cached formulas from a list.
static void	FormulaUtil.sortBySourceFile(List<Formula> forms)

Constructors in com.articulate.sigma with parameters of type Formula

Modifier	Constructor	Description
	Formula(Formula f)	Constructor to build a formula from an existing formula.

Constructor parameters in com.articulate.sigma with type arguments of type Formula

Modifier	Constructor	Description
	Derivation(String op, List<Formula> par)

Uses of Formula in com.articulate.sigma.nlg

Methods in com.articulate.sigma.nlg with parameters of type Formula

Modifier and Type	Method	Description
void	StackElement.argsInit(Formula formula, List<String> args)	Init the formulaArgs for this StackElement.
static String	NLGUtils.expandStar(Formula f, String strFormat, String lang)	This method expands all "star" (asterisk) directives in the input format string, and returns a new format string with individually numbered argument pointers.
void	LanguageFormatterStack.insertFormulaArgs(Formula formula)	Insert the given formula arguments into the topmost element of the stack.
void	LanguageFormatterStack.translateCurrProcessInstantiation(KB kb, Formula formula)	If possible, translate the process instantiation and insert the translation into the topmost stack element.

Constructors in com.articulate.sigma.nlg with parameters of type Formula

Modifier	Constructor	Description
	SumoProcessEntityProperty(Formula form)

Uses of Formula in com.articulate.sigma.parsing

Subclasses of Formula in com.articulate.sigma.parsing

Modifier and Type	Class	Description
class	FormulaAST

Methods in com.articulate.sigma.parsing with parameters of type Formula

Modifier and Type	Method	Description
static SuokifVisitor	SuokifVisitor.parseFormula(Formula input)	Parse a single formula and use this SuokifVisitor to process as the cached information for the formula.
static SuokifVisitor	SuokifApp.process(Formula fast)	Process the given SUO-KIF

Uses of Formula in com.articulate.sigma.tp

Method parameters in com.articulate.sigma.tp with type arguments of type Formula

Modifier and Type	Method	Description
boolean	EProver.assertFormula(String userAssertionTPTP, KB kb, EProver eprover, List<Formula> parsedFormulas, boolean tptp)	Add an assertion for inference.
static boolean	LEO.assertFormula(String userAssertionTPTP, KB kb, List<Formula> parsedFormulas, boolean tptp)	Add an assertion for inference.
static boolean	Vampire.assertFormula(String userAssertionTPTP, KB kb, List<Formula> parsedFormulas, boolean tptp)	Add an assertion for inference.

Uses of Formula in com.articulate.sigma.trans

Fields in com.articulate.sigma.trans declared as Formula

Modifier and Type	Field	Description
Formula	SUMOformulaToTPTPformula._f

Fields in com.articulate.sigma.trans with type parameters of type Formula

Modifier and Type	Field	Description
static Map<String,Formula>	SUMOKBtoTPTPKB.axiomKey
static Set<Formula>	THFnew.badUsageSymbols

Methods in com.articulate.sigma.trans that return Formula

Modifier and Type	Method	Description
static Formula	THFnew.adjustArity(KB kb, Formula f)	Adding the world argument messes up pre-processing for variable arity relations, so we have to decrement the numerical suffix as a hack.
static Formula	TPTP2SUMO.collapseConnectives(Formula form)	Remove binary cascading or's, xor's and and's and consolidate as single connectives with more arguments.
Formula	TPTP3ProofProcessor.extractAnswerClause(Formula ax)	*************************************************************** Return the answer clause, or null if not present
static Formula	Modals.handleHOL3pred(Formula f, KB kb, Integer worldNum)	Handle the predicates given in regHOL3pred, which have a parameter followed by a formula.
static Formula	Modals.handleHOLpred(Formula f, KB kb, Integer worldNum)	Handle predicates in regHOLpred that take an individual and a formula argument, e.g.
static Formula	Modals.handleModalAttribute(Formula f, KB kb, Integer worldNum)	Handle the predicate modalAttribute: (modalAttribute F M) is read as: "F holds in all worlds accessible via modality M".
static Formula	SUMOtoTFAform.instantiateNumericConstants(Formula f)	Substitute the values of numeric constants for their names.
static Formula	Modals.processModals(Formula f, KB kb)
static Formula	Modals.processRecurse(Formula f, KB kb, Integer worldNum)

Methods in com.articulate.sigma.trans with parameters of type Formula

Modifier and Type	Method	Description
static Formula	THFnew.adjustArity(KB kb, Formula f)	Adding the world argument messes up pre-processing for variable arity relations, so we have to decrement the numerical suffix as a hack.
static Formula	TPTP2SUMO.collapseConnectives(Formula form)	Remove binary cascading or's, xor's and and's and consolidate as single connectives with more arguments.
static String	SUMOtoTFAform.elimUnitaryLogops(Formula f)	Recursive routine to eliminate occurrences of 'forall', 'exists', 'invalid input: '<'=>', '=>', 'and', 'xor' and 'or' that have only one or zero arguments
static boolean	THFnew.exclude(Formula f, KB kb, Writer out)	Decide whether to exclude a formula from THF export.
static boolean	THFnew.excludeNonModal(Formula f, KB kb, Writer out)
Formula	TPTP3ProofProcessor.extractAnswerClause(Formula ax)	*************************************************************** Return the answer clause, or null if not present
boolean	SUMOKBtoTPTPKB.filterAxiom(Formula form, String tptp, PrintWriter pw)	Deprecated.
boolean	SUMOKBtoTPTPKB.filterAxiom(Formula form, String tptp, List<String> fileContents)
boolean	SUMOKBtoTPTPKB.filterExcludePredicates(Formula formula)
static String	SUMOtoTFAform.findType(Formula f)
static void	SUMOformulaToTPTPformula.generateQList(Formula f)
static String	THFnew.generateQList(Formula f, Map<String,Set<String>> typeMap, Set<String> vars)
static String	THFnew.generateQListNonModal(Formula f, Map<String,Set<String>> typeMap, Set<String> vars)
static Formula	Modals.handleHOL3pred(Formula f, KB kb, Integer worldNum)	Handle the predicates given in regHOL3pred, which have a parameter followed by a formula.
static Formula	Modals.handleHOLpred(Formula f, KB kb, Integer worldNum)	Handle predicates in regHOLpred that take an individual and a formula argument, e.g.
static Formula	Modals.handleModalAttribute(Formula f, KB kb, Integer worldNum)	Handle the predicate modalAttribute: (modalAttribute F M) is read as: "F holds in all worlds accessible via modality M".
static String	TPTPutil.htmlTPTPFormat(Formula f, String hyperlink, boolean traditionalLogic)	Format a formula for either text or HTML presentation by inserting the proper hyperlink code, characters for indentation and end of line.
static Formula	SUMOtoTFAform.instantiateNumericConstants(Formula f)	Substitute the values of numeric constants for their names.
static boolean	SUMOtoTFAform.isNumeric(Formula f)	a number, a variable with a numeric type or a function symbol or function with a numeric type
static String	THFnew.makeWorldVar(KB kb, Formula f)
Set<String>	SUMOtoTFAform.missingSorts(Formula f)
protected static String	SUMOtoTFAform.modifyPrecond(Formula f)	remove statements of the form (instance ?X term) if 'term' is Integer or RealNumber and ?X is already of that type in the quantifier list for the formula
protected static String	SUMOtoTFAform.modifyTypesToConstraints(Formula f)	replace type statements of the form (instance ?X term), where term is a subtype of Integer or RealNumber with a constraint that defines that type
static String	SUMOtoTFAform.numTypePromotion(Formula f, String parentType)	if the formula is a numeric atom or variable or a function with a number range and that type is more specific that the parentType, promote it with $to_real or invalid input: '&to_rat'
String	THF.oneKIF2THF(Formula form, boolean conjecture, KB kb)
static void	THFnew.oneTrans(KB kb, Formula f, PrintWriter bw)
static void	THFnew.oneTransNonModal(KB kb, Formula f, Writer bw)
static String	SUMOformulaToTPTPformula.process(Formula f, boolean query)	This is the primary method of the class.
static String	SUMOtoTFAform.process(Formula f, boolean query)	This is the primary method of the class.
static String	THFnew.process(Formula f, Map<String,Set<String>> typeMap, boolean query)	This is the primary method of the class.
static String	SUMOformulaToTPTPformula.processEquals(Formula f, Formula car, List<String> args)
static String	THFnew.processEquals(Formula f, Formula car, List<String> args, Map<String,Set<String>> typeMap)
static String	SUMOformulaToTPTPformula.processLogOp(Formula f, Formula car, List<String> args)
static String	THFnew.processLogOp(Formula f, Formula car, List<String> args, Map<String,Set<String>> typeMap)
static Formula	Modals.processModals(Formula f, KB kb)
static String	THFnew.processNonModal(Formula f, Map<String,Set<String>> typeMap, boolean query)
static Formula	Modals.processRecurse(Formula f, KB kb, Integer worldNum)
static String	SUMOformulaToTPTPformula.processRecurse(Formula f)
static String	SUMOtoTFAform.processRecurse(Formula f, String parentType)	process a formula into TF0
static String	THFnew.processRecurse(Formula f, Map<String,Set<String>> typeMap)
Set<String>	SUMOformulaToTPTPformula.tptpParse(Formula input, boolean query, KB kb)	Deprecated.
void	SUMOformulaToTPTPformula.tptpParse(Formula input, boolean query, KB kb, Set<Formula> preProcessedForms)	Deprecated.
static boolean	SUMOtoTFAform.typeConflict(Formula f)	Reject formulas that wind up with type conflicts despite all attempts to resolve them
String	SUMOKBtoTPTPKB.writeFile(String fileName, Formula conjecture, boolean isQuestion, PrintWriter pw)	Write all axioms in the KB to TPTP format.

Method parameters in com.articulate.sigma.trans with type arguments of type Formula

Modifier and Type	Method	Description
String	KIF2DB.getAllRels(Collection<Formula> forms)
List<String>	THF.KIF2THF(Collection<Formula> axiomsC, Collection<Formula> conjecturesC, KB kb)	The main function to convert KIF problems into TPTP THF representation; see the explanation at top of this file.
static Collection<String>	SUMOtoTFAform.processList(Collection<Formula> l)
void	SUMOformulaToTPTPformula.tptpParse(Formula input, boolean query, KB kb, Set<Formula> preProcessedForms)	Deprecated.

Uses of Formula in com.articulate.sigma.wordNet

Methods in com.articulate.sigma.wordNet with parameters of type Formula

Modifier and Type	Method	Description
void	WordNet.synsetFromTermFormat(Formula form, String tf, String SUMOterm, KB kb)	Generate a new synset from a termFormat statement