Formula

java.lang.Object
- com.articulate.sigma.Formula

All Implemented Interfaces:

java.io.Serializable, java.lang.Comparable
```
public class Formula
extends java.lang.Object
implements java.lang.Comparable, java.io.Serializable
```
Handle operations on an individual formula. This includes formatting for presentation as well as pre-processing for sending to the inference engine.

See Also:

Serialized Form

Field Summary

Fields
Modifier and Type	Field and Description
`static java.lang.String`	`AND`
`static java.lang.String`	`classSymbolSuffix`
`static java.lang.String`	`DIVIDEFN`
`static java.util.List<java.lang.String>`	`DOC_PREDICATES`
`long`	`endFilePosition` The length of the file in bytes at the position immediately after the end of the formula.
`int`	`endLine` The line in the file on which the formula ends.
`static java.lang.String`	`EQUAL`
`static java.lang.String`	`EQUANT`
`java.util.TreeSet<java.lang.String>`	`errors`
`static java.lang.String`	`FN_SUFF`
`static java.lang.String`	`GT`
`static java.lang.String`	`GTET`
`static java.lang.String`	`IF`
`static java.lang.String`	`IFF`
`static java.lang.String`	`KAPPAFN`
`static java.lang.String`	`LOG_FALSE`
`static java.lang.String`	`LOG_TRUE`
`static java.util.List<java.lang.String>`	`LOGICAL_OPERATORS` The SUO-KIF logical operators.
`static java.lang.String`	`LP`
`static java.lang.String`	`LT`
`static java.lang.String`	`LTET`
`protected static int`	`MAX_PREDICATE_ARITY` This constant indicates the maximum predicate arity supported by the current implementation of Sigma.
`static java.lang.String`	`MINUSFN`
`static java.lang.String`	`NOT`
`static java.lang.String`	`OR`
`static java.lang.String`	`PLUSFN`
`static java.lang.String`	`R_PREF`
`static java.lang.String`	`RP`
`static java.lang.String`	`RVAR`
`static java.lang.String`	`SK_PREF`
`static java.lang.String`	`SKFN`
`java.lang.String`	`sourceFile` The source file in which the formula appears.
`static java.lang.String`	`SPACE`
`int`	`startLine` The line in the file on which the formula starts.
`static java.lang.String`	`termMentionSuffix`
`static java.lang.String`	`termSymbolPrefix`
`static java.lang.String`	`termVariablePrefix`
`java.lang.String`	`theFormula` The formula in textual forms.
`java.util.ArrayList<java.lang.String>`	`theTptpFormulas` A list of TPTP formulas (Strings) that together constitute the translation of theFormula.
`static java.lang.String`	`TIMESFN`
`static java.lang.String`	`UQUANT`
`static java.lang.String`	`V_PREF`
`static java.lang.String`	`VVAR`
`static java.lang.String`	`VX`
`java.util.TreeSet<java.lang.String>`	`warnings` Warnings found during execution.

Constructor Summary

Constructors
Constructor and Description
`Formula()`
`Formula(Formula f)` Constructor to build a formula from an existing formula.
`Formula(java.lang.String f)` Just set the textual version of the formula

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`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<java.lang.String>`	`argumentsToArrayList(int start)` Return all the arguments in a simple formula as a list, starting at the given argument.
`boolean`	`atom()` Test whether the Formula is a LISP atom.
`static boolean`	`atom(java.lang.String s)` Test whether the String is a LISP atom.
`java.lang.String`	`badQuantification()` Not yet implemented! Test whether the Formula has variables that are not properly quantified.
`java.lang.String`	`caddr()` Returns the LISP 'caddr' of the formula, which is the third list element of the formula.
`java.lang.String`	`cadr()` Returns the LISP 'cadr' (the second list element) of the formula.
`java.lang.String`	`car()`
`Formula`	`carAsFormula()` Returns the LISP 'car' of the formula as a new Formula, if possible, else returns null.
`java.lang.String`	`cddr()` Returns the LISP 'cddr' of the formula - the rest of the rest, or the list minus its first two elements.
`Formula`	`cddrAsFormula()` Returns the LISP 'cddr' of the formula as a new Formula, if possible, else returns null.
`java.lang.String`	`cdr()` Return the LISP 'cdr' of the formula - the rest of a list minus its first element.
`Formula`	`cdrAsFormula()` Returns the LISP 'cdr' of the formula as a new Formula, if possible, else returns null.
`void`	`clearTheClausalForm()` This method clears the list of clauses that together constitute the resolution form of this Formula, and can be used in preparation for recomputing the clauses.
`void`	`clearTheTptpFormulas()` Clears theTptpFormulas if the ArrayList exists, else does nothing.
`java.util.Set<java.lang.String>`	`collectAllVariables()` Collects all variables in this Formula.
`java.util.ArrayList<java.lang.String>`	`collectExistentiallyQuantifiedVariables()` Collects all quantified variables in this Formula.
`java.util.ArrayList<java.util.ArrayList<java.lang.String>>`	`collectQuantifiedUnquantifiedVariables()` A new method to collect all quantified and unquantified variables in this Formula.
`void`	`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.ArrayList<java.lang.String>`	`collectQuantifiedVariables()` Collects all quantified variables in this Formula.
`java.util.Set<java.lang.String>`	`collectTerms()` Collect all the terms in a formula
`java.util.ArrayList<java.lang.String>`	`collectUnquantifiedVariables()` Collect all the unquantified variables in a formula
`java.util.ArrayList<java.util.ArrayList<java.lang.String>>`	`collectVariables()` Collects all variables in this Formula.
`int`	`compareTo(java.lang.Object f)` Implement the Comparable interface by defining the compareTo method.
`java.util.ArrayList<java.lang.String>`	`complexArgumentsToArrayList(int start)` Return all the arguments in a formula as a list, starting at the given argument.
`Formula`	`cons(Formula f)`
`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`	`copy()` Copy the Formula.
`java.lang.String`	`createID()`
`Formula`	`deepCopy()`
`boolean`	`deepEquals(Formula f)` Test if the contents of the formula are equal to the argument.
`boolean`	`empty()` Test whether the Formula is an empty list.
`static boolean`	`empty(java.lang.String s)` Test whether the String is an empty formula.
`boolean`	`equals(java.lang.Object o)` Test if the contents of the formula are equal to the argument.
`boolean`	`equals(java.lang.String s)` Test if the contents of the formula are equal to the String argument.
`java.lang.String`	`format(java.lang.String hyperlink, java.lang.String indentChars, java.lang.String eolChars)` Format a formula for either text or HTML presentation by inserting the proper hyperlink code, characters for indentation and end of line.
`java.util.HashSet<java.lang.String>`	`gatherRelationConstants()` Returns a HashSet of all atomic KIF Relation constants that occur as Predicates or Functions (argument 0 terms) in this Formula.
`java.util.HashMap<java.lang.String,java.util.ArrayList>`	`gatherRelationsWithArgTypes(KB kb)` Returns a HashMap in which the keys are the Relation constants gathered from this Formula, and the values are ArrayLists in which the ordinal positions 0 - n are occupied by the names of the corresponding argument types.
`java.lang.String`	`getArgument(int argnum)` Return the numbered argument of the given formula.
`java.util.ArrayList`	`getClauses()` Returns a List of List objects.
`protected static java.lang.String`	`getDualOperator(java.lang.String op)` Returns the dual logical operator of op, or null if op is not an operator or has no dual.
`java.util.TreeSet<java.lang.String>`	`getErrors()`
`java.lang.String`	`getSourceFile()`
`java.util.ArrayList`	`getTheClausalForm()` Returns a List of the clauses that together constitute the resolution form of this Formula.
`java.util.ArrayList<java.lang.String>`	`getTheTptpFormulas()` Returns an ArrayList of the TPTP formulas (Strings) that together constitute the TPTP translation of theFormula.
`java.util.HashMap`	`getVarMap()` Returns a map of the variable renames that occurred during the translation of this Formula into the clausal (resolution) form accessible via this.getClauses().
`int`	`hashCode()` If equals is overridden, hashCode must use the same "significant" fields.
`java.lang.String`	`htmlFormat(KB kb, java.lang.String href)` Format a formula for HTML presentation.
`java.lang.String`	`htmlFormat(java.lang.String html)` Format a formula for HTML presentation.
`boolean`	`isBalancedList()` Returns true if the Formula contains no unbalanced parentheses or unbalanced quote characters, otherwise returns false.
`boolean`	`isBinary()` Returns true if formula is a simple binary relation (note that because the argument list includes the predicate, which is argument 0, there will be three elements)
`boolean`	`isCached()` Test whether the Formula is automatically created by caching
`static boolean`	`isCommutative(java.lang.String obj)` A static utility method.
`static boolean`	`isComparisonOperator(java.lang.String term)` Returns true if term is a SUO-KIF predicate for comparing two (typically numeric) terms, else returns false.
`boolean`	`isExistentiallyQuantified()` Tests if this formula is an existentially quantified formula
`static boolean`	`isFunction(java.lang.String term)` Returns true if term is a SUO-KIF function, else returns false.
`boolean`	`isFunctionalTerm()` Test whether a Formula is a functional term.
`static boolean`	`isFunctionalTerm(java.lang.String s)` Test whether a Formula is a functional term
`boolean`	`isGround()` Returns true if formula does not have variables, else returns false.
`static boolean`	`isGround(java.lang.String form)` Returns true if formula is a valid formula with no variables, else returns false.
`boolean`	`isHigherOrder()` Test whether a Formula contains a Formula as an argument to other than a logical operator.
`boolean`	`isHorn(KB kb)` Returns true only if this Formula, is a horn clause or is simply modified to be horn by breaking out a conjunctive conclusion.
`static boolean`	`isLogicalOperator(java.lang.String term)` Returns true if term is a standard FOL logical operator, else returns false.
`static boolean`	`isMathFunction(java.lang.String term)` Returns true if term is a SUO-KIF mathematical function, else returns false.
`static boolean`	`isNegatedQuery(java.lang.String query, java.lang.String formulaString)` Compare the given formula to the negated query and return whether they are the same (minus the negation).
`static boolean`	`isQuantifier(java.lang.String pred)` Test whether a predicate is a logical quantifier
`static boolean`	`isQuantifierList(java.lang.String listPred, java.lang.String previousPred)` Test whether a list with a predicate is a quantifier list
`static boolean`	`isQuery(java.lang.String query, java.lang.String formula)` Compare the given formula to the query and return whether they are the same.
`boolean`	`isRule()` Returns true only if this Formula, explicitly quantified or not, starts with "=>" or "<=>", else returns false.
`boolean`	`isSimpleClause(KB kb)` Test whether a Formula is a simple list of terms (including functional terms).
`boolean`	`isSimpleNegatedClause(KB kb)` Test whether a Formula is a simple clause wrapped in a negation.
`static boolean`	`isSkolemTerm(java.lang.String term)` Returns true if term is a SUO-KIF Skolem term, else returns false.
`static boolean`	`isTerm(java.lang.String term)` Returns true if term is a valid SUO-KIF term, else returns false.
`boolean`	`isUniversallyQuantified()` Tests if this formula is an universally quantified formula
`boolean`	`isVariable()` Test whether the Formula is a variable
`static boolean`	`isVariable(java.lang.String term)` Test whether a String formula is a variable
`int`	`listLength()` Returns a non-negative int value indicating the top-level list length of this Formula if it is a proper listP(), else returns -1.
`boolean`	`listP()` Test whether the Formula is a list.
`static boolean`	`listP(java.lang.String s)` Test whether the String is a list.
`java.util.ArrayList<java.lang.String>`	`literalToArrayList()`
`boolean`	`logicallyEquals(Formula f)` Tests if this is logically equal with the parameter formula.
`boolean`	`logicallyEquals(java.lang.String s)` Test if the contents of the formula are equal to the argument at a deeper level than a simple string equals.
`static void`	`main(java.lang.String[] args)` A test method.
`java.lang.String`	`makeQuantifiersExplicit(boolean query)` Makes implicit quantification explicit.
`static java.util.List<java.util.Set<VariableMapping>>`	`mapFormulaVariables(Formula f1, Formula f2, KB kb, java.util.HashMap<FormulaUtil.FormulaMatchMemoMapKey,java.util.List<java.util.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`	`negate()`
`static java.lang.String`	`postProcess(java.lang.String s)` Remove the 'holds' prefix wherever it appears.
`void`	`read(java.lang.String s)` Read a String into the variable 'theFormula'.
`Formula`	`rename(java.lang.String term2, java.lang.String term1)` Replace term2 with term1
`Formula`	`renameVariableArityRelations(KB kb, java.util.TreeMap<java.lang.String,java.lang.String> relationMap)`
`Formula`	`replaceQuantifierVars(java.lang.String quantifier, java.util.List<java.lang.String> vars)`
`Formula`	`replaceVar(java.lang.String v, java.lang.String term)` Replace v with term.
`void`	`setSourceFile(java.lang.String filename)`
`Formula`	`substituteVariables(java.util.Map<java.lang.String,java.lang.String> m)` Replace variables with a value as given by the map argument
`static void`	`testArg2ArrayList()` A test method.
`static void`	`testBigArgs()` A test method.
`static void`	`testCar1()` A test method.
`static void`	`testClausifier(java.lang.String[] args)` A test method.
`static void`	`testCollectVariables()` A test method.
`static void`	`testComplexArgs()` A test method.
`static void`	`testIsSimpleClause()` A test method.
`static void`	`testReplaceVar()` A test method.
`static java.lang.String`	`textFormat(java.lang.String input)` Format a formula for text presentation.
`java.lang.String`	`toProlog()` Format a formula as a prolog statement.
`java.lang.String`	`toString()` Format a formula for text presentation.
`java.lang.String`	`toStringMeta()` Format a formula for text presentation include file and line#.
`boolean`	`unifyWith(Formula f)` Compares this formula with the parameter by trying to compare the predicate structure of th two and logically unify their variables.
`java.lang.String`	`validArgs()` Test whether the Formula uses logical operators and predicates with the correct number of arguments.
`java.lang.String`	`validArgs(java.lang.String filename, java.lang.Integer lineNo)` Test whether the Formula uses logical operators and predicates with the correct number of arguments.

Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait

- Field Detail
  - AND
```
public static final java.lang.String AND
```
    See Also:
    
    Constant Field Values
  - OR
```
public static final java.lang.String OR
```
    See Also:
    
    Constant Field Values
  - NOT
```
public static final java.lang.String NOT
```
    See Also:
    
    Constant Field Values
  - IF
```
public static final java.lang.String IF
```
    See Also:
    
    Constant Field Values
  - IFF
```
public static final java.lang.String IFF
```
    See Also:
    
    Constant Field Values
  - UQUANT
```
public static final java.lang.String UQUANT
```
    See Also:
    
    Constant Field Values
  - EQUANT
```
public static final java.lang.String EQUANT
```
    See Also:
    
    Constant Field Values
  - EQUAL
```
public static final java.lang.String EQUAL
```
    See Also:
    
    Constant Field Values
  - GT
```
public static final java.lang.String GT
```
    See Also:
    
    Constant Field Values
  - GTET
```
public static final java.lang.String GTET
```
    See Also:
    
    Constant Field Values
  - LT
```
public static final java.lang.String LT
```
    See Also:
    
    Constant Field Values
  - LTET
```
public static final java.lang.String LTET
```
    See Also:
    
    Constant Field Values
  - KAPPAFN
```
public static final java.lang.String KAPPAFN
```
    See Also:
    
    Constant Field Values
  - PLUSFN
```
public static final java.lang.String PLUSFN
```
    See Also:
    
    Constant Field Values
  - MINUSFN
```
public static final java.lang.String MINUSFN
```
    See Also:
    
    Constant Field Values
  - TIMESFN
```
public static final java.lang.String TIMESFN
```
    See Also:
    
    Constant Field Values
  - DIVIDEFN
```
public static final java.lang.String DIVIDEFN
```
    See Also:
    
    Constant Field Values
  - SKFN
```
public static final java.lang.String SKFN
```
    See Also:
    
    Constant Field Values
  - SK_PREF
```
public static final java.lang.String SK_PREF
```
    See Also:
    
    Constant Field Values
  - FN_SUFF
```
public static final java.lang.String FN_SUFF
```
    See Also:
    
    Constant Field Values
  - V_PREF
```
public static final java.lang.String V_PREF
```
    See Also:
    
    Constant Field Values
  - R_PREF
```
public static final java.lang.String R_PREF
```
    See Also:
    
    Constant Field Values
  - VX
```
public static final java.lang.String VX
```
    See Also:
    
    Constant Field Values
  - VVAR
```
public static final java.lang.String VVAR
```
    See Also:
    
    Constant Field Values
  - RVAR
```
public static final java.lang.String RVAR
```
    See Also:
    
    Constant Field Values
  - LP
```
public static final java.lang.String LP
```
    See Also:
    
    Constant Field Values
  - RP
```
public static final java.lang.String RP
```
    See Also:
    
    Constant Field Values
  - SPACE
```
public static final java.lang.String SPACE
```
    See Also:
    
    Constant Field Values
  - LOG_TRUE
```
public static final java.lang.String LOG_TRUE
```
    See Also:
    
    Constant Field Values
  - LOG_FALSE
```
public static final java.lang.String LOG_FALSE
```
    See Also:
    
    Constant Field Values
  - LOGICAL_OPERATORS
```
public static final java.util.List<java.lang.String> LOGICAL_OPERATORS
```
    The SUO-KIF logical operators.
  - DOC_PREDICATES
```
public static final java.util.List<java.lang.String> DOC_PREDICATES
```
  - sourceFile
```
public java.lang.String sourceFile
```
    The source file in which the formula appears.
  - startLine
```
public int startLine
```
    The line in the file on which the formula starts.
  - endLine
```
public int endLine
```
    The line in the file on which the formula ends.
  - endFilePosition
```
public long endFilePosition
```
    The length of the file in bytes at the position immediately after the end of the formula. This value is used only for formulas entered via KB.tell(). In general, you should not count on it being set to a value other than -1L.
  - errors
```
public java.util.TreeSet<java.lang.String> errors
```
  - warnings
```
public java.util.TreeSet<java.lang.String> warnings
```
    Warnings found during execution.
  - theFormula
```
public java.lang.String theFormula
```
    The formula in textual forms.
  - termMentionSuffix
```
public static final java.lang.String termMentionSuffix
```
    See Also:
    
    Constant Field Values
  - classSymbolSuffix
```
public static final java.lang.String classSymbolSuffix
```
    See Also:
    
    Constant Field Values
  - termSymbolPrefix
```
public static final java.lang.String termSymbolPrefix
```
    See Also:
    
    Constant Field Values
  - termVariablePrefix
```
public static final java.lang.String termVariablePrefix
```
    See Also:
    
    Constant Field Values
  - theTptpFormulas
```
public java.util.ArrayList<java.lang.String> theTptpFormulas
```
    A list of TPTP formulas (Strings) that together constitute the translation of theFormula. This member is a List, because predicate variable instantiation and row variable expansion might cause theFormula to expand to several TPTP formulas.
  - MAX_PREDICATE_ARITY
```
protected static final int MAX_PREDICATE_ARITY
```
    This constant indicates the maximum predicate arity supported by the current implementation of Sigma.
    
    See Also:
    
    Constant Field Values
- Constructor Detail
  - Formula
```
public Formula(Formula f)
```
    Constructor to build a formula from an existing formula. This isn't a complete deepCopy() since it leaves out the errors and warnings variables
  - Formula
```
public Formula()
```
  - Formula
```
public Formula(java.lang.String f)
```
    Just set the textual version of the formula
- Method Detail
  - getSourceFile
```
public java.lang.String getSourceFile()
```
  - setSourceFile
```
public void setSourceFile(java.lang.String filename)
```
  - getErrors
```
public java.util.TreeSet<java.lang.String> getErrors()
```
  - getTheTptpFormulas
```
public java.util.ArrayList<java.lang.String> getTheTptpFormulas()
```
    Returns an ArrayList of the TPTP formulas (Strings) that together constitute the TPTP translation of theFormula.
    
    Returns:
    
    An ArrayList of Strings, or an empty ArrayList if no translations have been created or entered.
  - clearTheTptpFormulas
```
public void clearTheTptpFormulas()
```
    Clears theTptpFormulas if the ArrayList exists, else does nothing.
  - getTheClausalForm
```
public java.util.ArrayList getTheClausalForm()
```
    Returns a List of the clauses that together constitute the resolution form of this Formula. The list could be empty if the clausal form has not yet been computed.
    
    Returns:
    
    ArrayList
  - clearTheClausalForm
```
public void clearTheClausalForm()
```
    This method clears the list of clauses that together constitute the resolution form of this Formula, and can be used in preparation for recomputing the clauses.
  - getClauses
```
public java.util.ArrayList getClauses()
```
    Returns a List of List objects. Each such object contains, in turn, a pair of List objects. Each List object in a pair contains Formula objects. The Formula objects contained in the first List object (0) of a pair represent negative literals (antecedent conjuncts). The Formula objects contained in the second List object (1) of a pair represent positive literals (consequent conjuncts). Taken together, all of the clauses constitute the resolution form of this Formula.
    
    Returns:
    
    A List of Lists.
  - getVarMap
```
public java.util.HashMap getVarMap()
```
    Returns a map of the variable renames that occurred during the translation of this Formula into the clausal (resolution) form accessible via this.getClauses().
    
    Returns:
    
    A Map of String (SUO-KIF variable) key-value pairs.
  - read
```
public void read(java.lang.String s)
```
    Read a String into the variable 'theFormula'.
  - createID
```
public java.lang.String createID()
```
    Returns:
    
    a unique ID by appending the hashCode() of the formula String to the file name in which it appears
  - copy
```
public Formula copy()
```
    Copy the Formula. This is in effect a deep copy although it ignores the errors and warnings variables.
  - deepCopy
```
public Formula deepCopy()
```
  - compareTo
```
public int compareTo(java.lang.Object f)
              throws java.lang.ClassCastException
```
    Implement the Comparable interface by defining the compareTo method. Formulas are equal if their formula strings are equal.
    
    Specified by:
    
    compareTo in interface java.lang.Comparable
    
    Throws:
    
    java.lang.ClassCastException
  - isBalancedList
```
public boolean isBalancedList()
```
    Returns true if the Formula contains no unbalanced parentheses or unbalanced quote characters, otherwise returns false.
    
    Returns:
    
    boolean
  - car
```
public java.lang.String car()
```
    Returns:
    
    the LISP 'car' of the formula as a String - the first element of the list. Note that this operation has no side effect on the Formula. Currently (10/24/2007) this method returns the empty string ("") when invoked on an empty list. Technically, this is wrong. In most LISPS, the car of the empty list is the empty list (or nil). But some parts of the Sigma code apparently expect this method to return the empty string when invoked on an empty list.
  - cdr
```
public java.lang.String cdr()
```
    Return the LISP 'cdr' of the formula - the rest of a list minus its first element. Note that this operation has no side effect on the Formula.
  - cons
```
public 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. This procedure is a little bit of a kluge, since this Formula is treated simply as a LISP object (presumably, a LISP list), and could be degenerate or malformed as a Formula. Note that this operation has no side effect on the original Formula.
    
    Parameters:
    
    obj - The String object that will become the 'car' (or head) of the resulting Formula (list).
    
    Returns:
    
    a new Formula, or the original Formula if the cons fails.
  - cons
```
public Formula cons(Formula f)
```
    Returns:
    
    a new Formula, or the original Formula if the cons fails.
  - cdrAsFormula
```
public Formula cdrAsFormula()
```
    Returns the LISP 'cdr' of the formula as a new Formula, if possible, else returns null. Note that this operation has no side effect on the Formula.
    
    Returns:
    
    a Formula, or null.
  - carAsFormula
```
public Formula carAsFormula()
```
    Returns the LISP 'car' of the formula as a new Formula, if possible, else returns null. Note that this operation has no side effect on the Formula.
    
    Returns:
    
    a Formula, or null.
  - cadr
```
public java.lang.String cadr()
```
    Returns the LISP 'cadr' (the second list element) of the formula. Note that this operation has no side effect on the Formula.
    
    Returns:
    
    a String, or the empty string if the is no cadr.
  - cddr
```
public java.lang.String cddr()
```
    Returns the LISP 'cddr' of the formula - the rest of the rest, or the list minus its first two elements. Note that this operation has no side effect on the Formula.
    
    Returns:
    
    a String, or null.
  - cddrAsFormula
```
public Formula cddrAsFormula()
```
    Returns the LISP 'cddr' of the formula as a new Formula, if possible, else returns null. Note that this operation has no side effect on the Formula.
    
    Returns:
    
    a Formula, or null.
  - caddr
```
public java.lang.String caddr()
```
    Returns the LISP 'caddr' of the formula, which is the third list element of the formula. Note that this operation has no side effect on the Formula.
    
    Returns:
    
    a String, or the empty string if there is no caddr.
  - append
```
public Formula append(Formula f)
```
    Returns the LISP 'append' of the formulas Note that this operation has no side effect on the Formula.
    
    Returns:
    
    a Formula
  - atom
```
public static boolean atom(java.lang.String s)
```
    Test whether the String is a LISP atom.
  - atom
```
public boolean atom()
```
    Test whether the Formula is a LISP atom.
  - empty
```
public boolean empty()
```
    Test whether the Formula is an empty list.
  - empty
```
public static boolean empty(java.lang.String s)
```
    Test whether the String is an empty formula. Not to be confused with a null string or empty string. There must be parentheses with nothing or whitespace in the middle.
  - listP
```
public boolean listP()
```
    Test whether the Formula is a list.
  - listP
```
public static boolean listP(java.lang.String s)
```
    Test whether the String is a list.
  - validArgs
```
public java.lang.String validArgs(java.lang.String filename,
                                  java.lang.Integer lineNo)
```
    Test whether the Formula uses logical operators and predicates with the correct number of arguments. "equals", "<=>", and "=>" are strictly binary. "or", and "and" are binary or greater. "not" is unary. "forall" and "exists" are unary with an argument list. Warn if we encounter a formula that has more arguments than MAX_PREDICATE_ARITY.
    
    Parameters:
    
    filename - If not null, denotes the name of the file being parsed.
    
    lineNo - If not null, indicates the location of the expression (formula) being parsed in the file being read.
    
    Returns:
    
    an empty String if there are no problems or an error message if there are.
  - validArgs
```
public java.lang.String validArgs()
```
    Test whether the Formula uses logical operators and predicates with the correct number of arguments. "equals", "<=>", and "=>" are strictly binary. "or", and "and" are binary or greater. "not" is unary. "forall" and "exists" are unary with an argument list. Warn if we encounter a formula that has more arguments than MAX_PREDICATE_ARITY.
    
    Returns:
    
    an empty String if there are no problems or an error message if there are.
  - badQuantification
```
public java.lang.String badQuantification()
```
    Not yet implemented! Test whether the Formula has variables that are not properly quantified. The case tested for is whether a quantified variable in the antecedent appears in the consequent or vice versa.
    
    Returns:
    
    an empty String if there are no problems or an error message if there are.
  - logicallyEquals
```
public boolean logicallyEquals(java.lang.String s)
```
    Test if the contents of the formula are equal to the argument at a deeper level than a simple string equals. The only logical manipulation is to treat conjunctions and disjunctions as unordered bags of clauses. So (and A B C) will be logicallyEqual(s) for example, to (and B A C). Note that this is a fairly time-consuming operation and should not generally be used for comparing large sets of formulas.
  - hashCode
```
public int hashCode()
```
    If equals is overridden, hashCode must use the same "significant" fields.
    
    Overrides:
    
    hashCode in class java.lang.Object
  - equals
```
public boolean equals(java.lang.Object o)
```
    Test if the contents of the formula are equal to the argument. Normalize all variables so that formulas can be equal independent of their variable names, which have no semantics.
    
    Overrides:
    
    equals in class java.lang.Object
  - equals
```
public boolean equals(java.lang.String s)
```
    Test if the contents of the formula are equal to the String argument. Normalize all variables.
  - logicallyEquals
```
public boolean logicallyEquals(Formula f)
```
    Tests if this is logically equal with the parameter formula. It employs three equality tests starting with the fastest and finishing with the slowest: - string comparisons: if the strings of the two formulae are equal return true as the formulae are also equal, otherwise try comparing them by more complex means - compare the predicate structure of the formulae (deepEquals(...)): this comparison only checks if the two formulae have an equal structure of predicates disregarding variable equivalence. Example: (and (instance ?A Human) (instance ?A Mushroom)) according to deepEquals(...) would be equal to (and (instance ?A Human) (instance ?B Mushroom)) even though the first formula refers only one variable but the second one refers two, and as such they are not logically equal. This method generates false positives, but only true negatives. If the result of the comparison is false, we return false, otherwise keep trying. - try to logically unify the formulae by matching the predicates and the variables
    
    Parameters:
    
    f -
    
    Returns:
  - unifyWith
```
public boolean unifyWith(Formula f)
```
    Compares this formula with the parameter by trying to compare the predicate structure of th two and logically unify their variables. The helper method mapFormulaVariables(....) returns a logical mapping between the variables of two formulae of one exists.
    
    Parameters:
    
    f -
    
    Returns:
  - mapFormulaVariables
```
public static java.util.List<java.util.Set<VariableMapping>> mapFormulaVariables(Formula f1,
                                                                                 Formula f2,
                                                                                 KB kb,
                                                                                 java.util.HashMap<FormulaUtil.FormulaMatchMemoMapKey,java.util.List<java.util.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. If a complete mapping is possible, it is returned. Each recursive call returns a list of sets of variable pairs. Each pair is a variable from the first formula and its potential corresponding variable in the second formula. Each set is a potential complete mapping between all the variables in the first formula and the ones in the second. The returned list contains all possible sets, so in essence all possible valid mappings of variables between the two formulas. The method will reconcile the list returned by all one level deeper recursive calls and return the list of sets which offer no contradictions. Note: for clauses with commutative
    
    Parameters:
    
    f1 -
    
    f2 -
    
    kb -
    
    memoMap - a memo-ization mechanism designed to reduce the number of recursive calls in "dynamic programming" fashion
    
    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
  - deepEquals
```
public boolean deepEquals(Formula f)
```
    Test if the contents of the formula are equal to the argument.
  - getArgument
```
public java.lang.String getArgument(int argnum)
```
    Return the numbered argument of the given formula. The first element of a formula (i.e. the predicate position) is number 0. Returns the empty string if there is no such argument position.
  - listLength
```
public int listLength()
```
    Returns a non-negative int value indicating the top-level list length of this Formula if it is a proper listP(), else returns -1. One caveat: This method assumes that neither null nor the empty string are legitimate list members in a wff. The return value is likely to be wrong if this assumption is mistaken.
    
    Returns:
    
    A non-negative int, or -1.
  - argumentsToArrayList
```
public java.util.ArrayList<java.lang.String> argumentsToArrayList(int start)
```
    Return all the arguments in a simple formula as a list, starting at the given argument. If formula is complex (i.e. an argument is a function or sentence), then return null. If the starting argument is greater than the number of arguments, also return null.
  - complexArgumentsToArrayList
```
public java.util.ArrayList<java.lang.String> complexArgumentsToArrayList(int start)
```
    Return all the arguments in a formula as a list, starting at the given argument. If the starting argument is greater than the number of arguments, return null.
  - collectVariables
```
public java.util.ArrayList<java.util.ArrayList<java.lang.String>> collectVariables()
```
    Collects all variables in this Formula. Returns an ArrayList containing a pair of ArrayLists. The first contains all explicitly quantified variables in the Formula. The second contains all variables in Formula that are not within the scope of some explicit quantifier.
    
    Returns:
    
    An ArrayList containing two ArrayLists, each of which could be empty
  - collectQuantifiedUnquantifiedVariables
```
public java.util.ArrayList<java.util.ArrayList<java.lang.String>> collectQuantifiedUnquantifiedVariables()
```
    A new method to collect all quantified and unquantified variables in this Formula. Return an ArrayList containing a pair of ArrayLists. The first contains all explicitly quantified varialbles. The second contains all variables that are not within the scope of some explicit quantifiers. This function is different from the old version collectVariables() in that it can keep track of some bad axioms where a variable is both in quantified list and unquantified list;
    
    Returns:
    
    An ArrayList containing two ArrayLists, each of which could be empty.
  - collectQuantifiedUnquantifiedVariablesRecurse
```
public void 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
  - collectAllVariables
```
public java.util.Set<java.lang.String> collectAllVariables()
```
    Collects all variables in this Formula. Returns an Set of String variable names (with initial '?'). Note that duplicates are not removed.
    
    Returns:
    
    An ArrayList of String variable names
  - collectExistentiallyQuantifiedVariables
```
public java.util.ArrayList<java.lang.String> collectExistentiallyQuantifiedVariables()
```
    Collects all quantified variables in this Formula. Returns an ArrayList of String variable names (with initial '?'). Note that duplicates are not removed.
    
    Returns:
    
    An ArrayList of String variable names
  - collectQuantifiedVariables
```
public java.util.ArrayList<java.lang.String> collectQuantifiedVariables()
```
    Collects all quantified variables in this Formula. Returns an ArrayList of String variable names (with initial '?'). Note that duplicates are not removed.
    
    Returns:
    
    An ArrayList of String variable names
  - collectUnquantifiedVariables
```
public java.util.ArrayList<java.lang.String> collectUnquantifiedVariables()
```
    Collect all the unquantified variables in a formula
  - collectTerms
```
public java.util.Set<java.lang.String> collectTerms()
```
    Collect all the terms in a formula
  - substituteVariables
```
public Formula substituteVariables(java.util.Map<java.lang.String,java.lang.String> m)
```
    Replace variables with a value as given by the map argument
  - makeQuantifiersExplicit
```
public java.lang.String makeQuantifiersExplicit(boolean query)
```
    Makes implicit quantification explicit.
    
    Parameters:
    
    query - controls whether to add universal or existential quantification. If true, add existential.
  - renameVariableArityRelations
```
public Formula renameVariableArityRelations(KB kb,
                                            java.util.TreeMap<java.lang.String,java.lang.String> relationMap)
```
    Parameters:
    
    kb - - The KB used to compute variable arity relations.
    
    relationMap - is a Map of String keys and values where the key is the renamed relation and the value is the original name. This is set as a side effect of this method.
    
    Returns:
    
    A new version of the Formula in which every VariableArityRelation has been renamed to include a numeric suffix corresponding to the actual number of arguments in the Formula.
  - gatherRelationsWithArgTypes
```
public java.util.HashMap<java.lang.String,java.util.ArrayList> gatherRelationsWithArgTypes(KB kb)
```
    Returns a HashMap in which the keys are the Relation constants gathered from this Formula, and the values are ArrayLists in which the ordinal positions 0 - n are occupied by the names of the corresponding argument types. n should never be greater than the value of Formula.MAX_PREDICATE_ARITY. For each Predicate key, the length of its ArrayList should be equal to the predicate's valence + 1. For each Function, the length of its ArrayList should be equal to its valence. Only Functions will have argument types in the 0th position of the ArrayList, since this position contains a function's range type. This means that all Predicate ArrayLists will contain at least one null value. A null value will also be added to the nth position of an ArrayList when no value can be obtained for that position.
    
    Returns:
    
    A HashMap that maps every Relation occurring in this Formula to an ArrayList indicating the Relation's argument types. Some HashMap keys may map to null values or empty ArrayLists, and most ArrayLists will contain some null values.
  - gatherRelationConstants
```
public java.util.HashSet<java.lang.String> gatherRelationConstants()
```
    Returns a HashSet of all atomic KIF Relation constants that occur as Predicates or Functions (argument 0 terms) in this Formula.
    
    Returns:
    
    a HashSet containing the String constants that denote KIF Relations in this Formula, or an empty HashSet.
  - isFunctionalTerm
```
public boolean isFunctionalTerm()
```
    Test whether a Formula is a functional term. Note this assumes the textual convention of all functions ending with "Fn".
  - isFunctionalTerm
```
public static boolean isFunctionalTerm(java.lang.String s)
```
    Test whether a Formula is a functional term
  - isHigherOrder
```
public boolean isHigherOrder()
```
    Test whether a Formula contains a Formula as an argument to other than a logical operator.
  - isVariable
```
public static boolean isVariable(java.lang.String term)
```
    Test whether a String formula is a variable
  - isVariable
```
public boolean isVariable()
```
    Test whether the Formula is a variable
  - isCached
```
public boolean isCached()
```
    Test whether the Formula is automatically created by caching
  - isRule
```
public boolean isRule()
```
    Returns true only if this Formula, explicitly quantified or not, starts with "=>" or "<=>", else returns false. It would be better to test for the occurrence of at least one positive literal with one or more negative literals, but this test would require converting the Formula to clausal form.
  - isHorn
```
public boolean isHorn(KB kb)
```
    Returns true only if this Formula, is a horn clause or is simply modified to be horn by breaking out a conjunctive conclusion.
  - isQuantifierList
```
public static boolean isQuantifierList(java.lang.String listPred,
                                       java.lang.String previousPred)
```
    Test whether a list with a predicate is a quantifier list
  - isSimpleClause
```
public boolean isSimpleClause(KB kb)
```
    Test whether a Formula is a simple list of terms (including functional terms).
  - isSimpleNegatedClause
```
public boolean isSimpleNegatedClause(KB kb)
```
    Test whether a Formula is a simple clause wrapped in a negation.
  - isQuantifier
```
public static boolean isQuantifier(java.lang.String pred)
```
    Test whether a predicate is a logical quantifier
  - isExistentiallyQuantified
```
public boolean isExistentiallyQuantified()
```
    Tests if this formula is an existentially quantified formula
    
    Returns:
  - isUniversallyQuantified
```
public boolean isUniversallyQuantified()
```
    Tests if this formula is an universally quantified formula
    
    Returns:
  - isCommutative
```
public static boolean isCommutative(java.lang.String obj)
```
    A static utility method.
    
    Parameters:
    
    obj - Any object, but should be a String.
    
    Returns:
    
    true if obj is a SUO-KIF commutative logical operator, else false.
  - getDualOperator
```
protected static java.lang.String getDualOperator(java.lang.String op)
```
    Returns the dual logical operator of op, or null if op is not an operator or has no dual.
    
    Parameters:
    
    op - A String, assumed to be a SUO-KIF logical operator
    
    Returns:
    
    A String, the dual operator of op, or null.
  - isLogicalOperator
```
public static boolean isLogicalOperator(java.lang.String term)
```
    Returns true if term is a standard FOL logical operator, else returns false.
    
    Parameters:
    
    term - A String, assumed to be an atomic SUO-KIF term.
  - isTerm
```
public static boolean isTerm(java.lang.String term)
```
    Returns true if term is a valid SUO-KIF term, else returns false.
    
    Parameters:
    
    term - A String, assumed to be an atomic SUO-KIF term.
  - isComparisonOperator
```
public static boolean isComparisonOperator(java.lang.String term)
```
    Returns true if term is a SUO-KIF predicate for comparing two (typically numeric) terms, else returns false.
    
    Parameters:
    
    term - A String.
  - isMathFunction
```
public static boolean isMathFunction(java.lang.String term)
```
    Returns true if term is a SUO-KIF mathematical function, else returns false.
    
    Parameters:
    
    term - A String.
  - isGround
```
public static boolean isGround(java.lang.String form)
```
    Returns true if formula is a valid formula with no variables, else returns false.
  - isGround
```
public boolean isGround()
```
    Returns true if formula does not have variables, else returns false.
  - isBinary
```
public boolean isBinary()
```
    Returns true if formula is a simple binary relation (note that because the argument list includes the predicate, which is argument 0, there will be three elements)
  - isFunction
```
public static boolean isFunction(java.lang.String term)
```
    Returns true if term is a SUO-KIF function, else returns false. Note that this test is purely syntactic, and could fail for functions that do not adhere to the convention of ending all functions with "Fn".
    
    Parameters:
    
    term - A String.
  - isSkolemTerm
```
public static boolean isSkolemTerm(java.lang.String term)
```
    Returns true if term is a SUO-KIF Skolem term, else returns false.
    
    Parameters:
    
    term - A String.
    
    Returns:
    
    true or false
  - literalToArrayList
```
public java.util.ArrayList<java.lang.String> literalToArrayList()
```
    Returns:
    
    An ArrayList (ordered tuple) representation of the Formula, in which each top-level element of the Formula is either an atom (String) or another list.
  - replaceVar
```
public Formula replaceVar(java.lang.String v,
                          java.lang.String term)
```
    Replace v with term. TODO: See if a regex replace is faster (commented out buggy code below)
  - replaceQuantifierVars
```
public Formula replaceQuantifierVars(java.lang.String quantifier,
                                     java.util.List<java.lang.String> vars)
                              throws java.lang.Exception
```
    Parameters:
    
    quantifier -
    
    vars -
    
    Returns:
    
    Throws:
    
    java.lang.Exception
  - isQuery
```
public static boolean isQuery(java.lang.String query,
                              java.lang.String formula)
```
    Compare the given formula to the query and return whether they are the same.
  - isNegatedQuery
```
public static boolean isNegatedQuery(java.lang.String query,
                                     java.lang.String formulaString)
```
    Compare the given formula to the negated query and return whether they are the same (minus the negation).
  - postProcess
```
public static java.lang.String postProcess(java.lang.String s)
```
    Remove the 'holds' prefix wherever it appears.
  - format
```
public java.lang.String format(java.lang.String hyperlink,
                               java.lang.String indentChars,
                               java.lang.String eolChars)
```
    Format a formula for either text or HTML presentation by inserting the proper hyperlink code, characters for indentation and end of line. A standard LISP-style pretty printing is employed where an open parenthesis triggers a new line and added indentation.
    
    Parameters:
    
    hyperlink - - the URL to be referenced to a hyperlinked term.
    
    indentChars - - the proper characters for indenting text.
    
    eolChars - - the proper character for end of line.
  - textFormat
```
public static java.lang.String textFormat(java.lang.String input)
```
    Format a formula for text presentation.
  - toString
```
public java.lang.String toString()
```
    Format a formula for text presentation.
    
    Overrides:
    
    toString in class java.lang.Object
  - toStringMeta
```
public java.lang.String toStringMeta()
```
    Format a formula for text presentation include file and line#.
  - htmlFormat
```
public java.lang.String htmlFormat(java.lang.String html)
```
    Format a formula for HTML presentation.
  - htmlFormat
```
public java.lang.String htmlFormat(KB kb,
                                   java.lang.String href)
```
    Format a formula for HTML presentation.
  - toProlog
```
public java.lang.String toProlog()
```
    Format a formula as a prolog statement. Note that only tuples are converted properly at this time. Statements with any embedded formulas or functions will be rejected with a null return.
  - rename
```
public Formula rename(java.lang.String term2,
                      java.lang.String term1)
```
    Replace term2 with term1
  - testClausifier
```
public static void testClausifier(java.lang.String[] args)
```
    A test method. It expects two command line arguments for the input file and output file.
  - testCollectVariables
```
public static void testCollectVariables()
```
    A test method.
  - testIsSimpleClause
```
public static void testIsSimpleClause()
```
    A test method.
  - testReplaceVar
```
public static void testReplaceVar()
```
    A test method.
  - testComplexArgs
```
public static void testComplexArgs()
```
    A test method.
  - testBigArgs
```
public static void testBigArgs()
```
    A test method.
  - testCar1
```
public static void testCar1()
```
    A test method.
  - testArg2ArrayList
```
public static void testArg2ArrayList()
```
    A test method.
  - negate
```
public Formula negate()
```
  - main
```
public static void main(java.lang.String[] args)
```
    A test method.

Class Formula

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

AND

OR

NOT

IF

IFF

UQUANT

EQUANT

EQUAL

GT

GTET

LT

LTET

KAPPAFN

PLUSFN

MINUSFN

TIMESFN

DIVIDEFN

SKFN

SK_PREF

FN_SUFF

V_PREF

R_PREF

VX

VVAR

RVAR

LP

RP

SPACE

LOG_TRUE

LOG_FALSE

LOGICAL_OPERATORS

DOC_PREDICATES

sourceFile

startLine

endLine

endFilePosition

errors

warnings

theFormula

termMentionSuffix

classSymbolSuffix

termSymbolPrefix

termVariablePrefix

theTptpFormulas

MAX_PREDICATE_ARITY

Constructor Detail

Formula

Formula

Formula

Method Detail

getSourceFile

setSourceFile

getErrors

getTheTptpFormulas

clearTheTptpFormulas

getTheClausalForm

clearTheClausalForm

getClauses

getVarMap

read

createID

copy

deepCopy

compareTo

isBalancedList

car

cdr

cons

cons

cdrAsFormula

carAsFormula

cadr

cddr

cddrAsFormula