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
com.articulate.sigma.semRewrite

Uses of Formula in com.articulate.sigma

Fields in com.articulate.sigma declared as Formula

Modifier and Type	Field and Description
Formula	SUMOformulaToTPTPformula._f

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

Modifier and Type	Field and Description
HashMap<String,Formula>	KIF.formulaMap A HashMap of String keys representing the formula, and Formula values.
HashMap<String,Formula>	KB.formulaMap A Map of all the Formula objects in the KB.

Methods in com.articulate.sigma that return Formula

Modifier and Type	Method and 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	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.
Formula	Formula.deepCopy()
Formula	KB.getFormulaByKey(String key) An accessor providing a Formula
Formula	Clausifier.instantiateVariables() Create constants to fill variables.
static Formula	KB.literalListToFormula(List<String> lit) Converts a literal (List object) to a Formula.
Formula	Formula.negate()
Formula	Formula.rename(String term2, String term1) Replace term2 with term1
Formula	Clausifier.rename(String term2, String term1) Replace term2 with term1
protected Formula	Formula.renameVariableArityRelations(KB kb, TreeMap<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	Formula.substituteVariables(Map<String,String> m) Replace variables with a value as given by the map argument
Formula	Clausifier.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 and Description
ArrayList<Formula>	KB.ask(String kind, int argnum, String term) Returns an ArrayList containing the Formulas that match the request.
ArrayList<Formula>	KB.askWithLiteral(Formula queryLit) This method retrieves formulas by asking the query expression queryLit, and returns the results, if any, in an ArrayList.
ArrayList<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.
ArrayList<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.
ArrayList<Formula>	KB.askWithRestriction(int argnum1, String term1, int argnum2, String term2)
ArrayList<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 ArrayList<Formula>	RowVars.expandRowVars(KB kb, Formula f) Expand row variables, keeping the information about the original source formula.
ArrayList<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)
ArrayList<Formula>	KB.merge(KIF kif, String pathname) Merges a KIF object containing a single formula into the current KB.
ArrayList<Formula>	FormulaPreprocessor.preProcess(Formula form, boolean isQuery, KB kb) Pre-process a formula before sending it to the theorem prover.
static ArrayList<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 ArrayList<Formula>	TaxoModel.removeCached(ArrayList<Formula> forms) Remove any cached formulas from a list.
ArrayList<Formula>	Clausifier.separateConjunctions() Turn a conjunction into an ArrayList of separate statements
static ArrayList<Formula>	Clausifier.separateConjunctions(Formula f) convenience method
static ArrayList<Formula>	KB.stringsToFormulas(List<String> strings) Converts all Strings in the input List to Formula objects.
static ArrayList<Formula>	KButilities.termIntersection(KB kb, String term1, String term2) Get all formulas that contain both terms.

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

Modifier and Type	Method and 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.
ArrayList<Formula>	KB.askWithLiteral(Formula queryLit) This method retrieves formulas by asking the query expression queryLit, and returns the results, if any, in an ArrayList.
static Formula	Clausifier.clausify(Formula f) convenience method
void	Formula.collectQuantifiedUnquantifiedVariablesRecurse(Formula f, HashMap<String,Boolean> varFlag, HashSet<String> unquantifiedVariables, HashSet<String> quantifiedVariables) Collect quantified and unquantified variables recursively
HashMap<String,HashSet<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.
HashMap<String,HashSet<String>>	FormulaPreprocessor.computeVariableTypesRecurse(KB kb, Formula f, HashMap<String,HashSet<String>> input)
Formula	Formula.cons(Formula f)
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 ArrayList<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
static boolean	SUMOKBtoTPTPKB.filterExcludePredicates(HashSet<String> excludedPredicates, Formula formula) return true if the given formula is simple clause, and contains one of the excluded predicates; otherwise return true;
HashMap<String,HashSet<String>>	FormulaPreprocessor.findExplicitTypes(Formula form) Collect variable names and their types from instance or subclass expressions.
void	FormulaPreprocessor.findExplicitTypesClasses(Formula form, HashMap<String,HashSet<String>> varExplicitTypes, HashMap<String,HashSet<String>> varExplicitClasses) Collect variable names and their types from instance or subclass expressions.
HashMap<String,HashSet<String>>	FormulaPreprocessor.findExplicitTypesClassesInAntecedent(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;
HashMap<String,HashSet<String>>	FormulaPreprocessor.findExplicitTypesInAntecedent(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(Formula form, boolean isNegativeLiteral, HashMap<String,HashSet<String>> varExplicitTypes, HashMap<String,HashSet<String>> varExplicitClasses) Recursively collect a variable name and its types.
protected static HashSet<String>	PredVarInst.gatherPredVars(Formula f) Collect and return all predicate variables for the given formula
static HashMap<String,Integer>	RowVars.getRowVarMaxAritiesWithOtherArgs(HashMap<String,HashSet<String>> ar, KB kb, Formula f) given in @param ar which is a list for each variable of all the predicates in which it appears as an argument, find the maximum arity allowed by predicate arities, as given by
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 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 Set<Formula>	PredVarInst.instantiatePredVars(Formula input, KB kb)
boolean	Formula.logicallyEquals(Formula f) Tests if this is logically equal with the parameter formula.
static List<Set<com.articulate.sigma.Formula.VariableMapping>>	Formula.mapFormulaVariables(Formula f1, Formula f2, KB kb, HashMap<FormulaUtil.FormulaMatchMemoMapKey,List<Set<com.articulate.sigma.Formula.VariableMapping>>> memoMap) Compares two formulae by recursively traversing its predicate structure and by building possible variable maps between the variables of the two formulae.
ArrayList<Formula>	FormulaPreprocessor.preProcess(Formula form, boolean isQuery, KB kb) Pre-process a formula before sending it to the theorem prover.
static Formula	Clausifier.renameVariables(Formula f) convenience method
static Formula	Clausifier.renameVariables(Formula f, Map topLevelVars, Map scopedRenames, Map allRenames) convenience method
static ArrayList<Formula>	Clausifier.separateConjunctions(Formula f) convenience method
static Formula	Clausifier.toCanonicalClausalForm(Formula f) convenience method
static ArrayList	Clausifier.toNegAndPosLitsWithRenameInfo(Formula f) convenience method
ArrayList<String>	SUMOformulaToTPTPformula.tptpParse(Formula input, boolean query, KB kb) Parse formulae into TPTP format
void	SUMOformulaToTPTPformula.tptpParse(Formula input, boolean query, KB kb, List<Formula> preProcessedForms) Parse formulae into TPTP format Result is returned in _f.theTptpFormulas
boolean	Formula.unifyWith(Formula f) Compares this formula with the parameter by trying to compare the predicate structure of th two and logically unify their variables.
static Formula	Clausifier.universalsOut(Formula f) convenience method
String	SUMOKBtoTPTPKB.writeTPTPFile(String fileName, Formula conjecture, boolean onlyPlainFOL, String reasoner) Sets isQuestion and calls writeTPTPFile() below
String	SUMOKBtoTPTPKB.writeTPTPFile(String fileName, Formula conjecture, boolean onlyPlainFOL, String reasoner, boolean isQuestion) Sets pw and calls writeTPTPFile() below
String	SUMOKBtoTPTPKB.writeTPTPFile(String fileName, Formula conjecture, boolean onlyPlainFOL, String reasoner, boolean isQuestion, PrintWriter pw) Write all axioms in the KB to TPTP format.

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

Modifier and Type	Method and Description
boolean	EProver.assertFormula(String userAssertionTPTP, KB kb, EProver eprover, ArrayList<Formula> parsedFormulas, boolean tptp) Add an assertion for inference.
static HashSet<String>	KBcache.collectArgFromFormulas(int arg, ArrayList<Formula> forms) Get the HashSet of the given arguments from an ArrayList of Formulas.
static String	HTMLformatter.formatFormulaList(ArrayList<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 ArrayList<ArrayList<String>>	KB.formulasToArrayLists(List<Formula> formulaList) Converts all Formula objects in the input List to ArrayList tuples.
String	THF.KIF2THF(Collection<Formula> axiomsC, Collection<Formula> conjecturesC, KB kb) public String KIF2THF(Collection axioms, Collection conjectures, KB kb) { // string builders for the essential results of the translation: // signature, axioms, and conjectures StringBuilder signatureResult = new StringBuilder(); signatureResult.append("\n%%% The extracted Signature %%%"); StringBuilder axiomsResult = new StringBuilder(); axiomsResult.append("\n\n%%% The translated axioms %%%"); StringBuilder conjecturesResult = new StringBuilder(); conjecturesResult.append("\n\n%%% The translated conjectures %%%"); // tags and a map to distinguish axioms from conjectures String axTag = "ax"; String conTag = "con"; HashMap taggedFormulas = new HashMap(); for (Iterator iter = axioms.iterator(); iter.hasNext();) { Formula ax = (Formula) iter.next(); taggedFormulas.put(ax,axTag); } for (Iterator iter = conjectures.iterator(); iter.hasNext();) { Formula con = (Formula) iter.next(); taggedFormulas.put(con,conTag); } // the main loop; we proceed formula by formula and work with side effects // to variables introduced above (I know that this is terrible programming style!) for (Iterator iter = taggedFormulas.keySet().iterator(); iter.hasNext();) { Formula form = (Formula) iter.next(); // formula f contains the explicitly quantified formula under // consideration, the quantifier (universal/existential) is // determined correctly for axioms and conjectures Formula f = new Formula(); if (taggedFormulas.get(form).equals(axTag)) { f.read(form.makeQuantifiersExplicit(false)); } else if (taggedFormulas.get(form).equals(conTag)) { f.read(form.makeQuantifiersExplicit(true)); } System.out.println("\nKIF2THF -- translating KIF formula: " + f.theFormula.trim()); // we request some semantic type-relevant information on the function and // relation symbols involved; this information is used with priority below HashMap relTypeInfo = f.gatherRelationsWithArgTypes(kb); // we initialize the terms-to-types mapping and start the actual translation terms = new HashMap(); String res = toTHF1(f,boolTp,relTypeInfo); // toTHF1 may return a THF translation that still contains many occurences // of the (kind of) polymorphic 'unkownTp' and in this case we apply further // translation attempts employing the incrementially refined term-to-type // information.
String	THF.KIF2THF(Collection<Formula> axiomsC, Collection<Formula> conjecturesC, KB kb) public String KIF2THF(Collection axioms, Collection conjectures, KB kb) { // string builders for the essential results of the translation: // signature, axioms, and conjectures StringBuilder signatureResult = new StringBuilder(); signatureResult.append("\n%%% The extracted Signature %%%"); StringBuilder axiomsResult = new StringBuilder(); axiomsResult.append("\n\n%%% The translated axioms %%%"); StringBuilder conjecturesResult = new StringBuilder(); conjecturesResult.append("\n\n%%% The translated conjectures %%%"); // tags and a map to distinguish axioms from conjectures String axTag = "ax"; String conTag = "con"; HashMap taggedFormulas = new HashMap(); for (Iterator iter = axioms.iterator(); iter.hasNext();) { Formula ax = (Formula) iter.next(); taggedFormulas.put(ax,axTag); } for (Iterator iter = conjectures.iterator(); iter.hasNext();) { Formula con = (Formula) iter.next(); taggedFormulas.put(con,conTag); } // the main loop; we proceed formula by formula and work with side effects // to variables introduced above (I know that this is terrible programming style!) for (Iterator iter = taggedFormulas.keySet().iterator(); iter.hasNext();) { Formula form = (Formula) iter.next(); // formula f contains the explicitly quantified formula under // consideration, the quantifier (universal/existential) is // determined correctly for axioms and conjectures Formula f = new Formula(); if (taggedFormulas.get(form).equals(axTag)) { f.read(form.makeQuantifiersExplicit(false)); } else if (taggedFormulas.get(form).equals(conTag)) { f.read(form.makeQuantifiersExplicit(true)); } System.out.println("\nKIF2THF -- translating KIF formula: " + f.theFormula.trim()); // we request some semantic type-relevant information on the function and // relation symbols involved; this information is used with priority below HashMap relTypeInfo = f.gatherRelationsWithArgTypes(kb); // we initialize the terms-to-types mapping and start the actual translation terms = new HashMap(); String res = toTHF1(f,boolTp,relTypeInfo); // toTHF1 may return a THF translation that still contains many occurences // of the (kind of) polymorphic 'unkownTp' and in this case we apply further // translation attempts employing the incrementially refined term-to-type // information.
static ArrayList<Formula>	TaxoModel.removeCached(ArrayList<Formula> forms) Remove any cached formulas from a list.
void	SUMOformulaToTPTPformula.tptpParse(Formula input, boolean query, KB kb, List<Formula> preProcessedForms) Parse formulae into TPTP format Result is returned in _f.theTptpFormulas

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

Constructor and Description
Formula(Formula f)

Uses of Formula in com.articulate.sigma.nlg

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

Modifier and Type	Method and Description
void	StackElement.argsInit(Formula formula, List<String> args) Init the formulaArgs for this StackElement.
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

Constructor and Description
SumoProcessEntityProperty(Formula form)

Uses of Formula in com.articulate.sigma.semRewrite

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

Modifier and Type	Field and Description
Formula	RHS.form

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

Modifier and Type	Method and Description
static String	Interpreter.formatAnswer(Formula query, List<String> inferenceAnswers, KB kb) generates the answer to a query by replacing the variables with the results from the inference call