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 |
Modifier and Type | Field and Description |
---|---|
Formula |
SUMOformulaToTPTPformula._f |
Modifier and Type | Field and Description |
---|---|
java.util.HashMap<java.lang.String,Formula> |
KIF.formulaMap
A HashMap of String keys representing the formula, and Formula values.
|
java.util.HashMap<java.lang.String,Formula> |
KB.formulaMap
A Map of all the Formula objects in the KB.
|
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(java.lang.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(java.lang.String key)
An accessor providing a Formula
|
Formula |
Clausifier.instantiateVariables()
Create constants to fill variables.
|
static Formula |
KB.literalListToFormula(java.util.List<java.lang.String> lit)
Converts a literal (List object) to a Formula.
|
Formula |
Formula.rename(java.lang.String term2,
java.lang.String term1)
Replace term2 with term1
|
Formula |
Clausifier.rename(java.lang.String term2,
java.lang.String term1)
Replace term2 with term1
|
protected Formula |
Formula.renameVariableArityRelations(KB kb,
java.util.TreeMap<java.lang.String,java.lang.String> relationMap) |
static Formula |
Clausifier.renameVariables(Formula f)
convenience method
|
static Formula |
Clausifier.renameVariables(Formula f,
java.util.Map topLevelVars,
java.util.Map scopedRenames,
java.util.Map allRenames)
convenience method
|
Formula |
Formula.replaceQuantifierVars(java.lang.String quantifier,
java.util.List<java.lang.String> vars) |
Formula |
Formula.replaceVar(java.lang.String v,
java.lang.String term)
Replace v with term.
|
Formula |
Formula.substituteVariables(java.util.Map<java.lang.String,java.lang.String> m)
Replace variables with a value as given by the map argument
|
Formula |
Clausifier.substituteVariables(java.util.Map<java.lang.String,java.lang.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
|
Modifier and Type | Method and Description |
---|---|
java.util.ArrayList<Formula> |
KB.ask(java.lang.String kind,
int argnum,
java.lang.String term)
Returns an ArrayList containing the Formulas that match the
request.
|
java.util.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.
|
java.util.ArrayList<Formula> |
KB.askWithLiteral(java.util.List<java.lang.String> queryLit)
This method retrieves Formulas by asking the query expression
queryLit, and returns the results, if any, in an ArrayList.
|
java.util.ArrayList<Formula> |
KB.askWithPredicateSubsumption(java.lang.String relation,
int idxArgnum,
java.lang.String idxTerm)
Returns an ArrayList containing the Formulae retrieved,
possibly via multiple asks that recursively use relation and
all of its subrelations.
|
java.util.ArrayList<Formula> |
KB.askWithRestriction(int argnum1,
java.lang.String term1,
int argnum2,
java.lang.String term2) |
java.util.ArrayList<Formula> |
KB.askWithTwoRestrictions(int argnum1,
java.lang.String term1,
int argnum2,
java.lang.String term2,
int argnum3,
java.lang.String term3)
Returns an ArrayList of Formulas in which the two terms
provided appear in the indicated argument positions.
|
static java.util.ArrayList<Formula> |
RowVars.expandRowVars(KB kb,
Formula f)
Expand row variables, keeping the information about the original
source formula.
|
java.util.ArrayList<Formula> |
KB.instancesOf(java.lang.String term)
Determine whether a particular term is an immediate instance,
which has a statement of the form (instance term otherTerm).
|
static java.util.Set<Formula> |
PredVarInst.instantiatePredVars(Formula input,
KB kb) |
java.util.ArrayList<Formula> |
FormulaPreprocessor.preProcess(Formula form,
boolean isQuery,
KB kb)
Pre-process a formula before sending it to the theorem prover.
|
static java.util.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 java.util.ArrayList<Formula> |
TaxoModel.removeCached(java.util.ArrayList<Formula> forms)
Remove any cached formulas from a list.
|
java.util.ArrayList<Formula> |
Clausifier.separateConjunctions()
Turn a conjunction into an ArrayList of separate statements
|
static java.util.ArrayList<Formula> |
Clausifier.separateConjunctions(Formula f)
convenience method
|
static java.util.ArrayList<Formula> |
KB.stringsToFormulas(java.util.List<java.lang.String> strings)
Converts all Strings in the input List to Formula objects.
|
static java.util.ArrayList<Formula> |
KButilities.termIntersection(KB kb,
java.lang.String term1,
java.lang.String term2)
Get all formulas that contain both terms.
|
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.
|
java.util.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,
java.util.HashMap<java.lang.String,java.lang.Boolean> varFlag,
java.util.HashSet<java.lang.String> unquantifiedVariables,
java.util.HashSet<java.lang.String> quantifiedVariables)
Collect quantified and unquantified variables recursively
|
java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.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.
|
java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.String>> |
FormulaPreprocessor.computeVariableTypesRecurse(KB kb,
Formula f,
java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.String>> input) |
Formula |
Formula.cons(Formula f) |
static java.lang.String |
Editor.createFormPage(KB kb,
java.lang.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 java.util.ArrayList<Formula> |
RowVars.expandRowVars(KB kb,
Formula f)
Expand row variables, keeping the information about the original
source formula.
|
static java.util.Set<java.lang.String> |
Clausifier.extractVariables(Formula f)
Extract all variables in a list
|
static boolean |
SUMOKBtoTPTPKB.filterExcludePredicates(java.util.HashSet<java.lang.String> excludedPredicates,
Formula formula)
return true if the given formula is simple clause,
and contains one of the excluded predicates;
otherwise return true;
|
java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.String>> |
FormulaPreprocessor.findExplicitTypes(Formula form)
Collect variable names and their types from instance or subclass
expressions.
|
void |
FormulaPreprocessor.findExplicitTypesClasses(Formula form,
java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.String>> varExplicitTypes,
java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.String>> varExplicitClasses)
Collect variable names and their types from instance or subclass
expressions.
|
java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.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;
|
java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.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,
java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.String>> varExplicitTypes,
java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.String>> varExplicitClasses)
Recursively collect a variable name and its types.
|
protected static java.util.HashSet<java.lang.String> |
PredVarInst.gatherPredVars(Formula f)
Collect and return all predicate variables for the given formula
|
static java.util.HashMap<java.lang.String,java.lang.Integer> |
RowVars.getRowVarMaxAritiesWithOtherArgs(java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.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 java.lang.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 java.lang.String |
TPTPutil.htmlTPTPFormat(Formula f,
java.lang.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 java.util.Set<Formula> |
PredVarInst.instantiatePredVars(Formula input,
KB kb) |
boolean |
Formula.logicallyEquals(Formula f)
Test if this is logically equal with the parameter formula
|
static java.util.List<java.util.Set<com.articulate.sigma.Formula.VariableMapping>> |
Formula.mapFormulaVariables(Formula f1,
Formula f2,
KB kb,
java.util.HashMap<FormulaUtil.FormulaMatchMemoMapKey,java.util.List<java.util.Set<com.articulate.sigma.Formula.VariableMapping>>> memoMap)
Compares recursively to formulas and returns possible variable maps between the variables of the two formulas
Returns:
null - if the formulas cannot be equals (due to having different predicates for example)
empty list- formulas are equal, but there are no variables to map
list 0f variable mapping sets the list of possible variable mapping sets which will make formulas equal
|
java.util.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,
java.util.Map topLevelVars,
java.util.Map scopedRenames,
java.util.Map allRenames)
convenience method
|
static java.util.ArrayList<Formula> |
Clausifier.separateConjunctions(Formula f)
convenience method
|
static Formula |
Clausifier.toCanonicalClausalForm(Formula f)
convenience method
|
static java.util.ArrayList |
Clausifier.toNegAndPosLitsWithRenameInfo(Formula f)
convenience method
|
java.util.ArrayList<java.lang.String> |
SUMOformulaToTPTPformula.tptpParse(Formula input,
boolean query,
KB kb)
Parse formulae into TPTP format
|
void |
SUMOformulaToTPTPformula.tptpParse(Formula input,
boolean query,
KB kb,
java.util.List<Formula> preProcessedForms)
Parse formulae into TPTP format
Result is returned in _f.theTptpFormulas
|
boolean |
Formula.unifyWith(Formula f) |
static Formula |
Clausifier.universalsOut(Formula f)
convenience method
|
java.lang.String |
SUMOKBtoTPTPKB.writeTPTPFile(java.lang.String fileName,
Formula conjecture,
boolean onlyPlainFOL,
java.lang.String reasoner)
Sets isQuestion and calls writeTPTPFile() below
|
java.lang.String |
SUMOKBtoTPTPKB.writeTPTPFile(java.lang.String fileName,
Formula conjecture,
boolean onlyPlainFOL,
java.lang.String reasoner,
boolean isQuestion)
Sets pw and calls writeTPTPFile() below
|
java.lang.String |
SUMOKBtoTPTPKB.writeTPTPFile(java.lang.String fileName,
Formula conjecture,
boolean onlyPlainFOL,
java.lang.String reasoner,
boolean isQuestion,
java.io.PrintWriter pw)
Write all axioms in the KB to TPTP format.
|
Modifier and Type | Method and Description |
---|---|
boolean |
EProver.assertFormula(java.lang.String userAssertionTPTP,
KB kb,
EProver eprover,
java.util.ArrayList<Formula> parsedFormulas,
boolean tptp)
Add an assertion for inference.
|
static java.util.HashSet<java.lang.String> |
KBcache.collectArgFromFormulas(int arg,
java.util.ArrayList<Formula> forms)
Get the HashSet of the given arguments from an ArrayList of Formulas.
|
static java.lang.String |
HTMLformatter.formatFormulaList(java.util.ArrayList<Formula> forms,
java.lang.String header,
KB kb,
java.lang.String language,
java.lang.String flang,
int start,
int localLimit,
java.lang.String limitString)
Create the HTML for a section of the Sigma term browser page.
|
static java.util.ArrayList<java.util.ArrayList<java.lang.String>> |
KB.formulasToArrayLists(java.util.List<Formula> formulaList)
Converts all Formula objects in the input List to ArrayList
tuples.
|
java.lang.String |
THF.KIF2THF(java.util.Collection<Formula> axiomsC,
java.util.Collection<Formula> conjecturesC,
KB kb)
public String KIF2THF(Collection
|
java.lang.String |
THF.KIF2THF(java.util.Collection<Formula> axiomsC,
java.util.Collection<Formula> conjecturesC,
KB kb)
public String KIF2THF(Collection
|
static java.util.ArrayList<Formula> |
TaxoModel.removeCached(java.util.ArrayList<Formula> forms)
Remove any cached formulas from a list.
|
void |
SUMOformulaToTPTPformula.tptpParse(Formula input,
boolean query,
KB kb,
java.util.List<Formula> preProcessedForms)
Parse formulae into TPTP format
Result is returned in _f.theTptpFormulas
|
Constructor and Description |
---|
Formula(Formula f) |
Modifier and Type | Method and Description |
---|---|
void |
StackElement.argsInit(Formula formula,
java.util.List<java.lang.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.
|
Constructor and Description |
---|
SumoProcessEntityProperty(Formula form) |
Modifier and Type | Field and Description |
---|---|
Formula |
RHS.form |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
Interpreter.formatAnswer(Formula query,
java.util.List<java.lang.String> inferenceAnswers,
KB kb) |