Package com.articulate.sigma

Class Formula

java.lang.Object
com.articulate.sigma.Formula
All Implemented Interfaces:
Serializable, Comparable
Direct Known Subclasses:
FormulaAST
public class Formula extends Object implements Comparable, 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:

  • Field Details

  • Constructor Details

    • 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(String f)
      Just set the textual version of the formula

  • Method Details

    • getSourceFile

      public String getSourceFile()

    • setSourceFile

      public void setSourceFile(String filename)

    • getLineNumber

      public int getLineNumber()

    • getErrors

      public Set<String> getErrors()

    • getTheTptpFormulas

      public Set<String> getTheTptpFormulas()
      Accessor method for backward compatibility. Returns the most recently populated TPTP cache: prefers TFF, then FOF, then legacy theTptpFormulas.

    • getFormula

      public String getFormula()
      the textual version of the formula

    • setFormula

      public void setFormula(String f)
      the textual version of the formula

    • createComment

      public static Formula createComment(String input)
      the textual version of the formula

    • printCaches

      public void printCaches()

    • getTheClausalForm

      public List 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 List 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 Map 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.

    • getVarTypes

      public Map<String,Set<String>> getVarTypes(KB kb)
      Returns a map of the variable types.
      Returns:
      A Map of String (SUO-KIF variable) key-value pairs.

    • getVarType

      public Set<String> getVarType(KB kb, String var)
      Returns the type of a variable or null if it doesn't exist.

    • read

      public void read(String s)
      Read a String into the variable 'theFormula'.

    • createID

      public 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(Object f) throws ClassCastException
      Implement the Comparable interface by defining the compareTo method. Formulas are equal if their formula strings are equal.
      Specified by:
      compareTo in interface Comparable
      Throws:
      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 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 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(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 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 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 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(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(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(String s)
      Test whether the String is a list.

    • validArgs

      public String validArgs(String filename, Integer lineNo)
      Test whether the Formula uses logical operators and predicates with the correct number of arguments. "equals", "invalid input: '<'=>", and "=>" are strictly binary. "or", "xor" 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 String validArgs()
      Test whether the Formula uses logical operators and predicates with the correct number of arguments. "equals", "invalid input: '<'=>", and "=>" are strictly binary. "or", "xor" 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

      @Deprecated public String badQuantification()
      Deprecated.
      TODO: 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

      @Deprecated public boolean logicallyEquals(String s)
      Deprecated.
      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 Object

    • equals

      public boolean equals(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 Object

    • equals

      public boolean equals(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 uses only one variable but the second one uses 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

      @Deprecated public boolean unifyWith(Formula f)
      Deprecated.
      Compares this formula with the parameter by trying to compare the predicate structure of the two and logically unify their variables. The helper method mapFormulaVariables(....) returns a logical mapping between the variables of two formulae of one exists.

    • mapFormulaVariables

      public static List<Set<VariableMapping>> 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. 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:
      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.

    • getStringArgument

      public String getStringArgument(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.

    • getArgument

      public Formula 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 null 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.

    • argumentsToArrayListString

      public List<String> argumentsToArrayListString(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.

    • argumentsToArrayList

      @Deprecated public List<Formula> argumentsToArrayList(int start)
      Deprecated.
      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. Deprecated - use complexArgumentsToArrayList()

    • complexArgumentsToArrayList

      public List<Formula> 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.

    • complexArgumentsToArrayListString

      public List<String> complexArgumentsToArrayListString(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 List<Set<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

    • collectQuantifiedUnquantifiedVariablesRecurse

      public void collectQuantifiedUnquantifiedVariablesRecurse(Formula f, Map<String,Boolean> varFlag, Set<String> unquantifiedVariables, Set<String> quantifiedVariables)
      Collect quantified and unquantified variables recursively

    • addAllNoDup

      public void addAllNoDup(Collection<String> thisCol, Collection<String> arg)
      Collects all String terms from one Collection and adds them to another, without duplication

    • collectAllVariables

      public Set<String> collectAllVariables()
      Collects all variables in this Formula. Returns an Set of String variable names (with initial '?').
      Returns:
      A Set of String variable names

    • collectAllVariablesOrdered

      public List<String> collectAllVariablesOrdered()
      Collects all variables in this Formula in lexical order. Returns an ArrayList of String variable names (with initial '?'). Note that unlike collectAllVariables() this is not cached and therefore potentially much slower, although it does fill the cache of variable names so using this method first, will make calls to collectAllVariables() fast if that method is called on the same formula after this method is called.
      Returns:
      An ArrayList of String variable names

    • collectQuantifiedVariables

      public Set<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 Set<String> collectUnquantifiedVariables()
      Collect all the unquantified variables in a formula

    • collectTerms

      public Set<String> collectTerms()
      Collect all the terms in a formula

    • substituteVariables

      public Formula substituteVariables(Map<String,String> m)
      Replace variables with a value as given by the map argument

    • makeQuantifiersExplicit

      public 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, Map<String,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 Map<String,List> 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 Set<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

      @Deprecated public boolean isFunctionalTerm()
      Deprecated.
      Test whether a Formula is a functional term. Note this assumes the textual convention of all functions ending with "Fn".

    • isFunctionalTerm

      @Deprecated public static boolean isFunctionalTerm(String s)
      Deprecated.
      Test whether a Formula is a functional term

    • isHigherOrder

      public boolean isHigherOrder(KB kb)
      Test whether a Formula contains a Formula as an argument to other than a logical operator. TODO: get var types in case there is a function variable, and copy that var type list down to the arguments

    • isVariable

      public static boolean isVariable(String term)
      Test whether a String formula is a variable

    • isVariable

      public boolean isVariable()
      Test whether the Formula is a variable

    • isRegularVariable

      public boolean isRegularVariable()
      Test whether the Formula is a regular '?' variable

    • isRowVar

      public boolean isRowVar()
      Test whether the Formula is a row 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 "invalid input: '<'=>", 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(String listPred, 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).
      Parameters:
      kb - the current knowledge base
      Returns:
      true if 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(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(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.

    • findType

      public String findType(KB kb)
      Returns:
      a String with the type(s) of the formula

    • getDualOperator

      protected static String getDualOperator(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.

    • isTrueFalse

      public static boolean isTrueFalse(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.

    • isLogicalOperator

      public static boolean isLogicalOperator(String term)
      Returns true if term is a constant true or constant false, else returns false.
      Parameters:
      term - A String, assumed to be an atomic SUO-KIF term.

    • isTerm

      public static boolean isTerm(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(String term)
      Returns true if term is a SUO-KIF predicate for comparing two (typically numeric) terms, else returns false.
      Parameters:
      term - A String.

    • isInequality

      public static boolean isInequality(String term)
      Returns true if term is a SUO-KIF inequality, else returns false.
      Parameters:
      term - A String.

    • isMathFunction

      public static boolean isMathFunction(String term)
      Returns true if term is a SUO-KIF mathematical function, else returns false.
      Parameters:
      term - A String.

    • isModal

      public boolean isModal(KB kb)

    • isEpistemic

      public boolean isEpistemic(KB kb)

    • isTemporal

      public boolean isTemporal(KB kb)

    • removeTemporalRelations

      public static String removeTemporalRelations(String p_f, KB kb)
      The purpose is to take simple HOL formula with temporal aspects and remove temporal aspects of it in an attempt to take it to FOL. Note: This may change the semantic meaning of the formal logic.

    • isOtherHOL

      public boolean isOtherHOL(KB kb)

    • isTFF

      public boolean isTFF(KB kb)

    • isGround

      public static boolean isGround(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

      @Deprecated public static boolean isFunction(String term)
      Deprecated.
      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(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 List<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(String v, String term)
      Replace v with term. TODO: See if a regex replace is faster (commented out buggy code below)

    • replaceQuantifierVars

      public Formula replaceQuantifierVars(String quantifier, List<String> vars) throws Exception
      Parameters:
      quantifier -
      vars -
      Returns:
      Throws:
      Exception

    • isQuery

      public static boolean isQuery(String query, String formula)
      Compare the given formula to the query and return whether they are the same.

    • isNegatedQuery

      public static boolean isNegatedQuery(String query, String formulaString)
      Compare the given formula to the negated query and return whether they are the same (minus the negation).

    • postProcess

      public static String postProcess(String s)
      Remove the 'holds' prefix wherever it appears.

    • format

      public String format(String hyperlink, String indentChars, 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 String textFormat(String input)
      Format a formula for text presentation.

    • toString

      public String toString()
      Format a formula for text presentation.
      Overrides:
      toString in class Object

    • toStringMeta

      public String toStringMeta()
      Format a formula for text presentation include file and line#.

    • htmlFormat

      public String htmlFormat(String html)
      Format a formula for HTML presentation.

    • htmlFormat

      public String htmlFormat(KB kb, String href)
      Format a formula for HTML presentation.

    • toProlog

      public 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(String term2, String term1)
      Replace term2 with term1

    • 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()

    • showHelp

      public static void showHelp()

    • main

      public static void main(String[] args) throws IOException
      Throws:
      IOException