Package com.articulate.sigma

Class KB

java.lang.Object
com.articulate.sigma.KB
All Implemented Interfaces:
Serializable
public class KB extends Object implements Serializable
***************************************************************** Contains methods for reading, writing knowledge bases and their configurations. Also contains the inference engine process for the knowledge base.
See Also:

  • Field Details

    • eprover

      public transient EProver eprover
      Eprover inference engine process for this KB.

    • leo

      public transient LEO leo
      LEO-III inference engine process for this KB.

    • name

      public String name
      The name of the knowledge base.

    • constituents

      public List<String> constituents
      An ArrayList of Strings that are the full canonical pathnames of the files that comprise the KB.

    • language

      public String language
      The natural language in which axiom paraphrases should be presented.

    • kbDir

      public String kbDir
      The location of preprocessed KIF files, suitable for loading into EProver.

    • celt

      public transient CELT celt
      The instance of the CELT process.

    • termDepthCache

      public Map<String,Integer> termDepthCache
      a cache built through lazy evaluation of the taxonomic depth of each term

    • terms

      public Set<String> terms
      A SortedSet of Strings, which are all the terms in the KB.

    • capterms

      public Map<String,String> capterms
      A Map from all uppercase terms to their possibly mixed case original versions

    • _userAssertionsString

      public static final String _userAssertionsString
      The String constant that is the suffix for file of user assertions.
      See Also:

    • _userAssertionsTPTP

      public static final String _userAssertionsTPTP
      The String constant that is the suffix for TPTP file of user assertions.
      See Also:

    • _userAssertionsTFF

      public static final String _userAssertionsTFF
      The String constant that is the suffix for TFF file of user assertions.
      See Also:

    • _userAssertionsTHF

      public static final String _userAssertionsTHF
      The String constant that is the suffix for THF file of user assertions.
      See Also:

    • _cacheFileSuffix

      public static final String _cacheFileSuffix
      The String constant that is the suffix for files of cached assertions.
      See Also:

    • formulaMap

      public Map<String,Formula> formulaMap
      A Map of all the Formula objects in the KB. Each key is a String representation of a Formula. Each value is the Formula object corresponding to the key.

    • formulas

      public Map<String,List<String>> formulas
      A HashMap of ArrayLists of String formulae, containing all the formulae in the KB. Keys are the formula itself, a formula ID, and term indexes created in KIF.createKey(). The actual formula can be retrieved by using the returned String as the key for the variable formulaMap

    • errors

      public Set<String> errors
      Errors found during loading of the KB constituents.

    • warnings

      public Set<String> warnings
      Warnings found during loading of the KB constituents.

    • modifiedContents

      public boolean modifiedContents
      Future: If true, the contents of the KB have been modified without updating the caches

    • kbCache

      public KBcache kbCache

    • axiomKey

      public static Map<String,Formula> axiomKey
      maps TPTP axiom IDs to SUMO formulas

    • termFrequency

      public Map<String,Integer> termFrequency

    • force

      public static boolean force
      force regeneration of TPTP file

    • debug

      public static boolean debug

    • dropOnePremiseFormulas

      public static boolean dropOnePremiseFormulas

    • modensPonens

      public static boolean modensPonens

    • loadFormatMapsAttempted

      protected List<String> loadFormatMapsAttempted
      This List is used to limit the number of warning messages logged by loadFormatMaps(lang). If an attempt to load format or termFormat values for lang is unsuccessful, the list is checked for the presence of lang. If lang is not in the list, a warning message is logged and lang is added to the list. The list is cleared whenever a constituent file is added or removed for KB, since the latter might affect the availability of format or termFormat values.

  • Constructor Details

    • KB

      public KB()

    • KB

      public KB(String n, String dir)
      Constructor which takes the name of the KB and the location where KBs preprocessed for EProver should be placed.

    • KB

      public KB(String n, String dir, boolean visibility)

    • KB

      public KB(KB kbIn) throws IOException
      Perform a deep copy of the kb input
      Parameters:
      kbIn -
      Throws:
      IOException

    • KB

      public KB(String n)
      Constructor

  • Method Details

    • withUserAssertionLock

      public <T> T withUserAssertionLock(Callable<T> c)

    • mergeKBs

      public void mergeKBs(KB kbIn)
      Experimental: Utility method to perform a merge with the KB input
      Parameters:
      kbIn - the KB to merge

    • isVisible

      public boolean isVisible()

    • getTerms

      public Set<String> getTerms()
      Returns a SortedSet of Strings, which are all the terms in the KB.

    • simplifyTerm

      public String simplifyTerm(String term, boolean ignoreCaps)
      Only called in BrowseBody.jsp when a single match is found. Purpose is to simplify a RegEx to its only matching term
      Parameters:
      term - a String
      Returns:
      modified term a String

    • containsRE

      public boolean containsRE(String term, boolean ignoreCaps)
      Takes a term (interpreted as a Regular Expression) and returns true if any term in the KB has a match with the RE.
      Parameters:
      term - A String
      Returns:
      true or false.

    • getREMatch

      public List<String> getREMatch(String term, boolean ignoreCaps)
      Takes a term (interpreted as a Regular Expression) and returns an ArrayList containing every term in the KB that has a match with the RE.
      Parameters:
      term - A String
      Returns:
      An ArrayList of terms that have a match to term

    • setTerms

      public void setTerms(Set<String> newTerms)
      Sets the synchronized SortedSet of all the terms in the KB to be kbTerms.

    • availableLanguages

      public List<String> availableLanguages()
      Get an ArrayList of Strings containing the language identifiers of available natural language formatting templates.
      Returns:
      an ArrayList of Strings containing the language identifiers

    • removeSuperClasses

      public Set<String> removeSuperClasses(Set<String> set)
      Remove from the given set any item which is a superclass of another item in the set.

    • checkArity

      public void checkArity()
      Arity errors should already have been trapped in addConstituent() unless a relation is used before it is defined. This routine is a comprehensive re-check.

    • getArgType

      public String getArgType(String reln, int argPos)
      Returns the type (SUO-KIF Class name) for any argument in argPos position of an assertion formed with the SUO-KIF Relation reln. If no argument type value is directly stated for reln, this method tries to find a value inherited from one of reln's super-relations.
      Parameters:
      reln - A String denoting a SUO-KIF Relation
      argPos - An int denoting an argument position, where 0 is the position of reln itself
      Returns:
      A String denoting a SUO-KIF Class, or null if no value can be obtained

    • getArgTypeClass

      public String getArgTypeClass(String reln, int argPos)
      Returns the type (SUO-KIF Class name) for any argument in argPos position of an assertion formed with the SUO-KIF Relation reln. If no argument type value is directly stated for reln, this method tries to find a value inherited from one of reln's super-relations.
      Parameters:
      reln - A String denoting a SUO-KIF Relation
      argPos - An int denoting an argument position, where 0 is the position of reln itself
      Returns:
      A String denoting a SUO-KIF Class, or null if no value can be obtained. A '+' is appended to the class name if the argument is a subclass of the class, rather than an instance

    • instancesOf

      public List<Formula> instancesOf(String term)
      Determine whether a particular term is an immediate instance, which has a statement of the form (instance term otherTerm). Note that this does not count for terms such as Attribute(s) and Relation(s), which may be defined as subAttribute(s) or subrelation(s) of another instance. If the term is not an instance, return an empty ArrayList. Otherwise, return an ArrayList of the Formula(s) in which the given term is defined as an instance. Note! This does not return instances of the given term, but rather the terms of which the given term is an instance.

    • instances

      public Set<String> instances(String term)
      Get all instances of a given term

    • isInstanceOf

      public boolean isInstanceOf(String i, String c)
      Returns true if i is an instance of c, else returns false.
      Parameters:
      i - A String denoting an instance.
      c - A String denoting a Class.
      Returns:
      true or false.

    • isAttribute

      public boolean isAttribute(String i)
      Returns true if i is an Attribute, else returns false.
      Parameters:
      i - A String denoting an possible instance of Attribute.
      Returns:
      true or false.

    • isChildOf

      public boolean isChildOf(String i, String c)
      Returns true if i is c, is an instance of c, or is subclass of c, or is subAttribute of c, else returns false. Note that every class is a child of itself
      Parameters:
      i - A String denoting a class or instance.
      c - A String denoting the parent Class.
      Returns:
      true or false.

    • isFunction

      public boolean isFunction(String i)
      Returns true if i is an instance of Function, else returns false.
      Parameters:
      i - A String denoting a constant.
      Returns:
      true or false.

    • isFunctional

      public boolean isFunctional(Formula form)
      Returns true if argument is functional expression, else returns false.
      Parameters:
      form - is a possibly functional literal.
      Returns:
      true or false.

    • isRelation

      public boolean isRelation(String i)
      Parameters:
      i - A String denoting an instance.
      Returns:
      true or false.

    • isRelationInAnyKB

      public static boolean isRelationInAnyKB(String i)
      Returns true if i is an instance of c in any loaded KB, else returns false.
      Parameters:
      i - A String denoting an instance.
      Returns:
      true or false.

    • isInstance

      public boolean isInstance(String term)

    • childOf

      public boolean childOf(String child, String parent)
      Determine whether a particular class or instance "child" is a child of the given "parent".
      Parameters:
      child - A String, the name of a term.
      parent - A String, the name of a term.
      Returns:
      true if child and parent constitute an actual or implied relation in the current KB, else false.

    • isSubclass

      public boolean isSubclass(String c1, String parent)
      Returns true if the subclass cache supports the conclusion that c1 is a subclass of c2, else returns false. Note that classes are also subclasses of themselves
      Parameters:
      c1 - A String, the name of a Class.
      parent - A String, the name of a Class.
      Returns:
      boolean

    • isSubAttribute

      public boolean isSubAttribute(String c1, String parent)
      Returns true if the KB cache supports the conclusion that c1 is a subAttribute of c2, else returns false.
      Parameters:
      c1 - A String, the name of a SetOrClass.
      parent - A String, the name of a SetOrClass.
      Returns:
      boolean

    • formulasToArrayLists

      public static List<List<String>> formulasToArrayLists(List<Formula> formulaList)
      Converts all Formula objects in the input List to ArrayList tuples.
      Parameters:
      formulaList - A list of Formulas.
      Returns:
      An ArrayList of formula tuples (ArrayLists), or an empty ArrayList.

    • atomsToFormulas

      public static List<Formula> atomsToFormulas(List<String> strings)

    • literalListToString

      public static String literalListToString(List<String> literal)
      Converts a literal (List object) to a String.
      Parameters:
      literal - A List representing a SUO-KIF formula.
      Returns:
      A String representing a SUO-KIF formula.

    • literalListToFormula

      public static Formula literalListToFormula(List<String> lit)
      Converts a literal (List object) to a Formula.
      Parameters:
      lit - A List representing a SUO-KIF formula.
      Returns:
      A SUO-KIF Formula object, or null if no Formula can be created.

    • getTermsViaAskWithRestriction

      public List<String> getTermsViaAskWithRestriction(int argnum1, String term1, int argnum2, String term2, int targetArgnum, Set<String> predicatesUsed)
      Returns an ArrayList containing the terms (Strings) that correspond to targetArgnum in the Formulas obtained from the method call askWithRestriction(argnum1, term1, argnum2, term2).
      Parameters:
      predicatesUsed - A Set to which will be added the predicates of the ground assertions actually used to gather the terms returned
      Returns:
      An ArrayList of terms, or an empty ArrayList if no terms can be retrieved.

    • getTermsViaAskWithRestriction

      public List<String> getTermsViaAskWithRestriction(int argnum1, String term1, int argnum2, String term2, int targetArgnum)
      Returns an ArrayList containing the terms (Strings) that correspond to targetArgnum in the Formulas obtained from the method call askWithRestriction(argnum1, term1, argnum2, term2).
      Returns:
      An ArrayList of terms, or an empty ArrayList if no terms can be retrieved.

    • getFirstTermViaAskWithRestriction

      public String getFirstTermViaAskWithRestriction(int argnum1, String term1, int argnum2, String term2, int targetArgnum)
      Returns the first term found that corresponds to targetArgnum in the Formulas obtained from the method call askWithRestriction(argnum1, term1, argnum2, term2).
      Returns:
      A SUO-KIF term (String), or null is no answer can be retrieved.

    • askWithRestriction

      public List<Formula> askWithRestriction(int argnum1, String term1, int argnum2, String term2)
      Returns:
      an ArrayList of Formulas in which the two terms provided appear in the indicated argument positions. If there are no Formula(s) matching the given terms and respective argument positions, return an empty ArrayList. Iterate through the smallest list of results.

    • askWithTwoRestrictions

      public List<Formula> askWithTwoRestrictions(int argnum1, String term1, int argnum2, String term2, int argnum3, String term3)
      Returns an ArrayList of Formulas in which the two terms provided appear in the indicated argument positions. If there are no Formula(s) matching the given terms and respective argument positions, return an empty ArrayList.
      Returns:
      ArrayList

    • getTermsViaAWTR

      public List<String> getTermsViaAWTR(int argnum1, String term1, int argnum2, String term2, int argnum3, String term3, int targetArgnum)
      Returns an ArrayList containing the SUO-KIF terms that match the request.
      Returns:
      An ArrayList of terms, or an empty ArrayList if no matches can be found.

    • getFirstTermViaAWTR

      public String getFirstTermViaAWTR(int argnum1, String term1, int argnum2, String term2, int argnum3, String term3, int targetArgnum)
      Returns the first SUO-KIF terms that matches the request, or null.
      Returns:
      A term (String), or null.

    • getTermsViaAsk

      public List<String> getTermsViaAsk(int knownArgnum, String knownArg, int targetArgnum)
      Returns an ArrayList containing the terms (Strings) that correspond to targetArgnum in the ground atomic Formulae in which knownArg is in the argument position knownArgnum. The ArrayList returned will contain no duplicate terms.
      Parameters:
      knownArgnum - The argument position of knownArg
      knownArg - The term that appears in the argument knownArgnum of the ground atomic Formulae in the KB
      targetArgnum - The argument position of the terms being sought
      Returns:
      An ArrayList of Strings, which will be empty if no match found.

    • ask

      public List<Formula> ask(String kind, int argnum, String term)
      Returns an ArrayList containing the Formulas that match the request.
      Parameters:
      kind - May be one of "ant", "cons", "stmt", or "arg"
      argnum - The argument position of the term being asked for. The first argument after the predicate is "1". This parameter is ignored if the kind is "ant", "cons" or "stmt".
      term - The term that appears in the statements being requested.
      Returns:
      An ArrayList of Formula(s), which will be empty if no match found. see KIF.createKey()

    • askWithPredicateSubsumption

      public List<Formula> askWithPredicateSubsumption(String relation, int idxArgnum, String idxTerm)
      Returns an ArrayList containing the Formulae retrieved, possibly via multiple asks that recursively use relation and all of its subrelations. Note that the Formulas might be formed with different predicates, but all of the predicates will be subrelations of relation and will be related to each other in a subsumption hierarchy.

      FIXME: this routine only gets subrelations one level down

      Parameters:
      relation - The name of a predicate, which is assumed to be the 0th argument of one or more atomic formulae
      idxArgnum - The argument position occupied by idxTerm in each ground Formula to be retrieved
      idxTerm - A constant that occupied idxArgnum position in each ground Formula to be retrieved
      Returns:
      an ArrayList of Formulas that satisfy the query, or an empty ArrayList if no Formulae are retrieved.

    • getTermsViaPredicateSubsumption

      public List<String> getTermsViaPredicateSubsumption(String relation, int idxArgnum, String idxTerm, int targetArgnum, boolean useInverses, Set predicatesUsed)
      Returns an ArrayList containing SUO-KIF constants, possibly retrieved via multiple asks that recursively use relation and all of its subrelations.
      Parameters:
      relation - The name of a predicate, which is assumed to be the 0th argument of one or more atomic Formulae
      idxArgnum - The argument position occupied by term in the ground atomic Formulae that will be retrieved to gather the target (answer) terms
      idxTerm - A constant that occupies idxArgnum position in each of the ground atomic Formulae that will be retrieved to gather the target (answer) terms
      targetArgnum - The argument position of the answer terms in the Formulae to be retrieved
      useInverses - If true, the inverses of relation and its subrelations will be also be used to try to find answer terms
      predicatesUsed - A Set to which will be added the predicates of the ground assertions actually used to gather the terms returned
      Returns:
      an ArrayList of terms (SUO-KIF constants), or an empty ArrayList if no terms can be retrieved

    • getTermsViaPredicateSubsumption

      public List<String> getTermsViaPredicateSubsumption(String relation, int idxArgnum, String idxTerm, int targetArgnum, boolean useInverses)
      Returns an ArrayList containing SUO-KIF constants, possibly retrieved via multiple asks that recursively use relation and all of its subrelations.
      Parameters:
      relation - The name of a predicate, which is assumed to be the 0th argument of one or more atomic Formulae
      idxArgnum - The argument position occupied by term in the ground atomic Formulae that will be retrieved to gather the target (answer) terms
      idxTerm - A constant that occupies idxArgnum position in each of the ground atomic Formulae that will be retrieved to gather the target (answer) terms
      targetArgnum - The argument position of the answer terms in the Formulae to be retrieved
      useInverses - If true, the inverses of relation and its subrelations will be also be used to try to find answer terms
      Returns:
      an ArrayList of terms (SUO-KIF constants), or an empty ArrayList if no terms can be retrieved

    • getFirstTermViaPredicateSubsumption

      public String getFirstTermViaPredicateSubsumption(String relation, int idxArgnum, String idxTerm, int targetArgnum, boolean useInverses)
      Returns the first SUO-KIF constant found via asks using relation and its subrelations.
      Parameters:
      relation - The name of a predicate, which is assumed to be the 0th argument of one or more atomic Formulae.
      idxArgnum - The argument position occupied by term in the ground atomic Formulae that will be retrieved to gather the target (answer) terms.
      idxTerm - A constant that occupies idxArgnum position in each of the ground atomic Formulae that will be retrieved to gather the target (answer) terms.
      targetArgnum - The argument position of the answer terms in the Formulae to be retrieved.
      useInverses - If true, the inverses of relation and its subrelations will be also be used to try to find answer terms.
      Returns:
      A SUO-KIF constants (String), or null if no term can be retrieved.

    • getTransitiveClosureViaPredicateSubsumption

      public List<String> getTransitiveClosureViaPredicateSubsumption(String relation, int idxArgnum, String idxTerm, int targetArgnum, boolean useInverses)
      Returns an ArrayList containing the transitive closure of relation starting from idxTerm in position idxArgnum. The result does not contain idxTerm.
      Parameters:
      relation - The name of a predicate, which is assumed to be the 0th argument of one or more atomic Formulae
      idxArgnum - The argument position occupied by term in the ground atomic Formulae that will be retrieved to gather the target (answer) terms
      idxTerm - A constant that occupies idxArgnum position in the first "level" of ground atomic Formulae that will be retrieved to gather the target (answer) terms
      targetArgnum - The argument position of the answer terms in the Formulae to be retrieved
      useInverses - If true, the inverses of relation and its subrelations will be also be used to try to find answer terms
      Returns:
      an ArrayList of terms (SUO-KIF constants), or an empty ArrayList if no terms can be retrieved

    • addAllSafe

      public void addAllSafe(Collection c1, Collection c2)
      Add all members of one collection to another. If the argument is null, do nothing.

    • getAllSub

      @Deprecated public Set<String> getAllSub(String term, String rel)
      Deprecated.
      Get all children of the given term following instance and subclass relations as well as the indicated rel

    • merge

      public List<Formula> merge(KIF kif, String pathname)
      Merges a KIF object containing a single formula into the current KB.
      Parameters:
      kif - A KIF object.
      pathname - The full, canonical pathname string of the constituent file in which the formula will be saved, if known.
      Returns:
      If any of the formulas are already present, returns an ArrayList containing the old (existing) formulas, else returns an empty ArrayList.

    • rename

      public void rename(String term2, String term1)
      Rename term2 as term1 throughout the knowledge base. This is an operation with side effects - the term names in the KB are changed.

    • writeTerms

      public void writeTerms() throws IOException
      Throws:
      IOException

    • tell

      public String tell(String input)
      Adds a formula to the knowledge base.
      Parameters:
      input - The String representation of a SUO-KIF Formula.
      Returns:
      A String indicating the status of the tell operation.

    • askEProver

      public EProver askEProver(String suoKifFormula, int timeout, int maxAnswers)
      Submits a query to the E inference engine.
      Parameters:
      suoKifFormula - The String representation of the SUO-KIF query.
      timeout - The number of seconds after which the inference engine should give up.
      maxAnswers - The maximum number of answers (binding sets) the inference engine should return.
      Returns:
      an instance of the EProver with results

    • askLeo

      public LEO askLeo(String suoKifFormula, int timeout, int maxAnswers)
      Submits a query to the inference engine.
      Parameters:
      suoKifFormula - The String representation of the SUO-KIF query.
      timeout - The number of seconds after which the inference engine should give up.
      maxAnswers - The maximum number of answers (binding sets) the inference engine should return.
      Returns:
      A String indicating the status of the ask operation.

    • askVampire

      public Vampire askVampire(String suoKifFormula, int timeout, int maxAnswers)
      Submits a query to the inference engine.
      Parameters:
      suoKifFormula - The String representation of the SUO-KIF query.
      timeout - The number of seconds after which the inference engine should give up.
      maxAnswers - The maximum number of answers (binding sets) the inference engine should return.
      Returns:
      A String indicating the status of the ask operation.

    • askVampireForTQ

      public Vampire askVampireForTQ(String suoKifFormula, int timeout, int maxAnswers, boolean modensPonens)

    • tellRequiresBaseRegeneration

      public boolean tellRequiresBaseRegeneration(String input)
      Return true if THIS input (about to be told) requires base regen.

    • tqRequiresBaseRegeneration

      public boolean tqRequiresBaseRegeneration()
      Return true if the current TQ user assertions require rebuilding the base SUMO.. Conservative v1: rebuild on schema changes or ground transitive facts.

    • askVampireModensPonens

      public Vampire askVampireModensPonens(String suoKifFormula, int timeout, int maxAnswers)
      STEPS: 1 - AskVampire to get the first output 2 - Process the output to keep only the authored axioms 3 - Send new command to vampire with Modens Ponens options 4 - If wanted drop the one premise formulas. 5 - Replace the new proof's infRules with the original ones. 6 - Return Vampire object for further processing from AskTell.jsp
      Parameters:
      suoKifFormula -
      timeout -
      maxAnswers -
      Returns:

    • askVampireTPTP

      public Vampire askVampireTPTP(String test_path, int timeout, int maxAnswers)
      Executes a Vampire theorem prover query on a given TPTP problem file. This method validates included files in TPTP format, processes the result by running multiple configurations of Vampire, and optionally applies modus ponens reasoning or drops one-premise formulas.
      Parameters:
      test_path - The file path to the TPTP problem file to be processed.
      timeout - The maximum amount of time (in seconds) allowed for the inference process.
      maxAnswers - The maximum number of answers to retrieve from the theorem prover.
      Returns:
      A Vampire object containing the results of the theorem prover execution, including output and proofs.

    • askVampireTHF

      public Vampire askVampireTHF(String test_path, int timeout, int maxAnswers)
      Executes the Vampire automated theorem prover with higher-order logic (HOL) mode on a given THF problem file. This method processes the includes and runs the Vampire prover with the specified parameters.
      Parameters:
      test_path - The file path of the TPTP problem to be processed.
      timeout - The maximum amount of time (in seconds) that Vampire is allowed to run.
      maxAnswers - The maximum number of answers that Vampire should produce (not currently used in logic).
      Returns:
      A Vampire instance populated with the results of the proof attempt.

    • askVampireHOL

      public Vampire askVampireHOL(String stmt, int timeout, int maxAnswers, boolean useModals)
      Ask Vampire HOL using the existing .thf axioms. Input : SUO-KIF query string (stmt). Output : Vampire object with HOL proof output.

    • askVampireFormat

      public String askVampireFormat(String suoKifFormula, int timeout, int maxAnswers)
      Return a SUMO-formatted proof string

    • askNoProof

      public List<String> askNoProof(String suoKifFormula, int timeout, int maxAnswers)
      Submits a query to the inference engine. Returns a list of answers from inference engine. If no proof is found, return null;
      Parameters:
      suoKifFormula - The String representation of the SUO-KIF query.
      Returns:
      A list of answers from inference engine; If no proof or answer is found, return null;

    • askEngine

      public String askEngine(String suoKifFormula, int timeout, int maxAnswers, InferenceEngine engine)
      ************************************************************* Submits a query to specified InferenceEngine object. Returns an XML formatted String that contains the response of the inference engine. It should be in the form "...".
      Parameters:
      suoKifFormula - The String representation of the SUO-KIF query.
      timeout - The number of seconds after which the underlying inference engine should give up. (Time taken by axiom selection doesn't count.)
      maxAnswers - The maximum number of answers (binding sets) the inference engine should return.
      engine - InferenceEngine object that will be used for the inference.
      Returns:
      A String indicating the status of the ask operation.

    • askSInE

      public String askSInE(String suoKifFormula, int timeout, int maxAnswers)
      Submits a query to the SInE inference engine. Returns an XML formatted String that contains the response of the inference engine. It should be in the form "...".
      Parameters:
      suoKifFormula - The String representation of the SUO-KIF query.
      timeout - The number of seconds after which the underlying inference engine should give up. (Time taken by axiom selection doesn't count.)
      maxAnswers - The maximum number of answers (binding sets) the inference engine should return.
      Returns:
      A String indicating the status of the ask operation.

    • termDepth

      public int termDepth(String term)
      Submits a query to the LEO inference engine. Returns an XML formatted String that contains the response of the inference engine. It should be in the form "...". suoKifFormula The String representation of the SUO-KIF query. timeout The number of seconds after which the underlying inference engine should give up. (Time taken by axiom selection doesn't count.) maxAnswers The maximum number of answers (binding sets) the inference engine should return.
      Returns:
      A String indicating the status of the ask operation. public String askLEOOld(String suoKifFormula, int timeout, int maxAnswers, String flag) { String result = ""; try { String LeoExecutable = KBmanager.getMgr().getPref("leoExecutable"); String LeoInput = KBmanager.getMgr().getPref("inferenceTestDir") + "prob.p"; String LeoProblem; String responseLine; String LeoOutput = ""; File LeoExecutableFile = new File(LeoExecutable); File LeoInputFile = new File(LeoInput); FileWriter LeoInputFileW = new FileWriter(LeoInput); List selectedQuery = new ArrayList(); Formula newQ = new Formula(); newQ.read(suoKifFormula); selectedQuery.add(newQ); List selFs = null; if (flag.equals("LeoSine")) { SInE sine = new SInE(this.formulaMap.keySet()); selFs = new ArrayList(sine.performSelection(suoKifFormula)); sine.terminate(); } else if (flag.equals("LeoLocal")) selFs = new ArrayList(); else if (flag.equals("LeoGlobal")) { selFs = new ArrayList(); Iterator it = this.formulaMap.values().iterator(); while (it.hasNext()) { Formula entry = it.next(); selFs.add(entry.toString()); } } try { // add user asserted formulas File dir = new File(this.kbDir); File file = new File(dir, (this.name + _userAssertionsString)); String filename = file.getCanonicalPath(); BufferedReader userAssertedInput = new BufferedReader(new FileReader(filename)); try { String line = null; / readLine is a bit quirky : it returns the content of a line MINUS the newline. it returns null only for the END of the stream. it returns an empty String if two newlines appear in a row. while ((line = userAssertedInput.readLine()) != null) selFs.add(line); } finally { userAssertedInput.close(); } } catch (IOException ex) { System.err.println("Error in KB.askLEO(): " + ex.getMessage()); ex.printStackTrace(); } List selectedFormulas = new ArrayList(); Formula newF = new Formula(); Iterator it = selFs.iterator(); while (it.hasNext()) { String entry = it.next(); newF = new Formula(); newF.read(entry); selectedFormulas.add(newF); } System.out.println(selFs.toString()); THF thf = new THF(); LeoProblem = thf.KIF2THF(selectedFormulas, selectedQuery, this); LeoInputFileW.write(LeoProblem); LeoInputFileW.close(); String command = LeoExecutableFile.getCanonicalPath() + " -po 1 -t " + timeout + Formula.SPACE + LeoInputFile.getCanonicalPath(); Process leo = Runtime.getRuntime().exec(command); BufferedReader reader = new BufferedReader(new InputStreamReader(leo.getInputStream())); while ((responseLine = reader.readLine()) != null) LeoOutput += responseLine + "\n"; reader.close(); System.out.println(LeoOutput); if (LeoOutput.contains("SZS status Theorem")) { result = "Answer 1. yes" + "

      " + LeoProblem.replaceAll("\\n", "
      ") + "

      " + LeoOutput.replaceAll("\\n", "
      "); } else { result = "Answer 1. don't know" + "

      " + LeoProblem.replaceAll("\\n", "
      ") + "

      " + LeoOutput.replaceAll("\\n", "
      "); } } catch (Exception ex) { System.err.println("Error in KB.askLEO(): " + ex.getMessage()); ex.printStackTrace(); } return result; } /***************************************************************** Count the number of "levels" deep the term is in taxonomic relations from Entity. Remove trailing '+' signs. Also handle a composite term like (UnionFn A B) with a warning

    • immediateParents

      public Set<String> immediateParents(String term)

    • compareTermDepth

      public int compareTermDepth(String t1, String t2)
      Analogous to compareTo(), return -1,0 or 1 depending on whether the first term is "smaller", equal to or "greater" than the second, respectively. A term that is the parent of another is "smaller". If not a parent of the other, the smaller term is that which is fewer "levels" from their common parent. Therefore, terms that are not the same can still be "equal" if they're at the same level of the taxonomy.

    • mostGeneralType

      public String mostGeneralType(Collection<String> terms)
      Find the most specific term in a collection using compareTermDepth()

    • mostSpecificType

      public String mostSpecificType(Collection<String> terms)
      Find the most specific term in a collection using compareTermDepth()

    • mostSpecificTerm

      public String mostSpecificTerm(Collection<String> terms)
      Find the most specific term in a collection using compareTermDepth()

    • containsTerm

      public boolean containsTerm(String term)
      Takes a term and returns true if the term occurs in the KB.
      Parameters:
      term - A String.
      Returns:
      true or false.

    • containsFile

      public boolean containsFile(String fname)
      Takes a filename without path and returns true if it occurs in the KB.
      Parameters:
      fname - A String.
      Returns:
      true or false.

    • containsFormula

      public boolean containsFormula(String formula)
      Takes a formula string and returns true if the corresponding Formula occurs in the KB.
      Parameters:
      formula - A String.
      Returns:
      true or false.

    • getCountTerms

      public int getCountTerms()
      Count the number of terms in the knowledge base in order to present statistics to the user.
      Returns:
      The int(eger) number of terms in the knowledge base.

    • getCountRelations

      public int getCountRelations()
      Count the number of relations in the knowledge base in order to present statistics to the user.
      Returns:
      The int(eger) number of relations in the knowledge base.

    • getCountAxioms

      public int getCountAxioms()
      Count the number of formulas in the knowledge base in order to present statistics to the user.
      Returns:
      The int(eger) number of formulas in the knowledge base.

    • getFormulas

      public TreeSet<String> getFormulas()
      An accessor providing a TreeSet of un-preProcessed String representations of Formulae.
      Returns:
      A TreeSet of Strings.

    • getFormulaByKey

      public Formula getFormulaByKey(String key)
      An accessor providing a Formula

    • getCountRules

      public int getCountRules()
      Count the number of rules in the knowledge base in order to present statistics to the user. Note that the number of rules is a subset of the number of formulas.
      Returns:
      The int(eger) number of rules in the knowledge base.

    • getNearestRelations

      public List<String> getNearestRelations(String term)
      Get the neighbors of this initial uppercase term (class or function).

    • getNearestNonRelations

      public List<String> getNearestNonRelations(String term)
      Get the neighbors of this initial lowercase term (relation).

    • getAlphaBefore

      public String getAlphaBefore(String term, int num)
      Get the alphabetically num lower neighbor of this initial term, which must exist in the current KB otherwise an empty string is returned.

    • getAlphaAfter

      public String getAlphaAfter(String term, int num)
      Get the alphabetically num higher neighbor of this initial term, which must exist in the current KB otherwise an empty string is returned.

    • loadFormatMaps

      public void loadFormatMaps(String lang)
      Populates the format maps for language lang. see termFormatMap is a HashMap of language keys and HashMap values. The interior HashMaps are term keys and format string values. see formatMap is the same but for relation format strings.

    • clearFormatMaps

      protected void clearFormatMaps()
      Clears all loaded format and termFormat maps, for all languages.

    • getTermFormatMap

      public Map<String,String> getTermFormatMap(String lang)
      This method creates a dictionary (Map) of SUO-KIF term symbols -- the keys -- and a natural language string for each key that is the preferred name for the term -- the values -- in the context denoted by lang. If the Map has already been built and the language hasn't changed, just return the existing map. This is a case of "lazy evaluation".
      Returns:
      An instance of Map where the keys are terms and the values are format strings.

    • getFormatMap

      public Map<String,String> getFormatMap(String lang)
      This method creates an association list (Map) of the natural language format string and the relation name for which that format string applies. If the map has already been built and the language hasn't changed, just return the existing map. This is a case of "lazy evaluation".
      Returns:
      An instance of Map where the keys are relation names and the values are format strings.

    • getTermFormatMapAll

      public Map<String,List<String>> getTermFormatMapAll(String lang)
      This method creates a dictionary (Map) of SUO-KIF term symbols -- the keys -- and a natural language list of strings for each key that is all the names for the term -- the values -- in the context denoted by lang. If the Map has already been built and the language hasn't changed, just return the existing map. This is a case of "lazy evaluation".
      Returns:
      An instance of Map where the keys are terms and the values are a list of format strings.

    • getFormatMapAll

      public Map<String,List<String>> getFormatMapAll(String lang)
      This method creates an association list (Map) of the natural language format string and a list of the relation name for which that format string applies. If the map has already been built and the language hasn't changed, just return the existing map. This is a case of "lazy evaluation".
      Returns:
      An instance of Map where the keys are relation names and the values are format strings.

    • getTermFormat

      public String getTermFormat(String lang, String term)
      Get the termFormat entry for a given term and language

    • deleteUserAssertionsForInference

      public void deleteUserAssertionsForInference()

    • deleteUserAssertions

      public void deleteUserAssertions() throws IOException
      Deletes user assertions, both in the files and in the constituents list.
      Throws:
      IOException

    • deleteUserAssertionsAndReload

      public void deleteUserAssertionsAndReload()
      Deletes the user assertions key in the constituents map, and then reloads the KBs.

    • readConstituent

      public KIF readConstituent(String filename)

    • addConstituentInfo

      public void addConstituentInfo(KIF file)
      Adds a formula or formulas into the KB
      Parameters:
      file - the KIF file to add to this KB

    • addConstituent

      public void addConstituent(String filename)
      Add a new KB constituent by reading in the file, and then merging the formulas with the existing set of formulas.
      Parameters:
      filename - - The full path of the file being added

    • reload

      public void reload()
      Reload all the KB constituents.

    • writeFile

      public void writeFile(String fname) throws IOException
      Write a KIF file consisting of all the formulas in the knowledge base.
      Parameters:
      fname - - the name of the file to write, including full path.
      Throws:
      IOException

    • writeConfiguration

      public SimpleElement writeConfiguration()
      Create the XML configuration element.

    • getCompiledPattern

      public static Pattern getCompiledPattern(String key)
      This method returns a compiled regular expression Pattern object indexed by key.
      Parameters:
      key - A String that is the retrieval key for a compiled regular expression Pattern.
      Returns:
      A compiled regular expression Pattern instance.

    • getPatternGroupIndex

      public static int getPatternGroupIndex(String key)
      This method returns the int value that identifies the regular expression binding group to be returned when there is a match.
      Parameters:
      key - A String that is the retrieval key for the binding group index associated with a compiled regular expression Pattern.
      Returns:
      An int that indexes a binding group.

    • getMatches

      public static List<String> getMatches(String input, String patternKey, ArrayList<String> accumulator)
      This method finds regular expression matches in an input string using a compiled Pattern and binding group index retrieved with patternKey. If the ArrayList accumulator is provided, match results are added to it and it is returned. If accumulator is not provided (is null), then a new ArrayList is created and returned if matches are found.
      Parameters:
      input - The input String in which matches are sought.
      patternKey - A String used as the retrieval key for a regular expression Pattern object, and an int index identifying a binding group.
      accumulator - An optional ArrayList to which matches are added. Note that if accumulator is provided, it will be the return value even if no new matches are found in the input String.
      Returns:
      An ArrayList, or null if no matches are found and an accumulator is not provided.

    • getMatches

      public static List<String> getMatches(String input, String patternKey)
      This method finds regular expression matches in an input string using a compiled Pattern and binding group index retrieved with patternKey, and returns the results, if any, in an ArrayList.
      Parameters:
      input - The input String in which matches are sought.
      patternKey - A String used as the retrieval key for a regular expression Pattern object, and an int index identifying a binding group.
      Returns:
      An ArrayList, or null if no matches are found.

    • askWithLiteral

      public List<Formula> askWithLiteral(List<String> queryLit)
      This method retrieves Formulas by asking the query expression queryLit, and returns the results, if any, in an ArrayList.
      Parameters:
      queryLit - The query, which is assumed to be a List (atomic literal) consisting of a single predicate and its arguments. The arguments could be variables, constants, or a mix of the two, but only the first constant encountered in a left to right sweep over the literal will be used in the actual query.
      Returns:
      An ArrayList of Formula objects, or an empty ArrayList if no answers are retrieved.

    • askWithLiteral

      public List<Formula> askWithLiteral(Formula queryLit)
      This method retrieves formulas by asking the query expression queryLit, and returns the results, if any, in an ArrayList.
      Parameters:
      queryLit - The query, which is assumed to be an atomic literal consisting of a single predicate and its arguments. The arguments could be variables, constants, or a mix of the two, but only the first constant encountered in a left to right sweep over the literal will be used in the actual query.
      Returns:
      An ArrayList of Formula objects, or an empty ArrayList if no answers are retrieved.

    • getAllSuperClasses

      public Set<String> getAllSuperClasses(Set<String> classNames)
      This method retrieves the upward transitive closure of all Class names contained in the input set. The members of the input set are not included in the result set.
      Parameters:
      classNames - A Set object containing SUO-KIF class names (Strings).
      Returns:
      A Set of SUO-KIF class names, which could be empty.

    • getAllInstances

      @Deprecated protected Set<String> getAllInstances(Set<String> classNames)
      Deprecated.
      This method retrieves all instances of the classes named in the input set. TODO: Deprecated since it seems to do the opposite of what it should.
      Parameters:
      classNames - A Set of String, containing SUO-KIF class names
      Returns:
      A TreeSet, possibly empty, containing SUO-KIF constant names.

    • getAllInstances

      public Set<String> getAllInstances(String className)
      This method retrieves all instances of the class named in the input String.
      Parameters:
      className - The name of a SUO-KIF Class.
      Returns:
      A TreeSet, possibly empty, containing SUO-KIF constant names.

    • getValence

      public int getValence(String relnName)
      This method tries to find or compute a valence for the input relation.
      Parameters:
      relnName - A String, the name of a SUO-KIF Relation.
      Returns:
      An int value. -1 means that no valence value could be found. 0 means that the relation is a VariableArityRelation. 1-5 are the standard SUO-KIF valence values.

    • collectPredicates

      public List<String> collectPredicates()
      Returns:
      an ArrayList containing all predicates in this KB.

    • isEmptyList

      public static boolean isEmptyList(Object obj)
      Parameters:
      obj - Any object
      Returns:
      true if obj is a String representation of a LISP empty list, else false.

    • isVariable

      public static boolean isVariable(String obj)
      A static utility method.
      Parameters:
      obj - Presumably, a String.
      Returns:
      true if obj is a SUO-KIF variable, else false.

    • isQuantifier

      public static boolean isQuantifier(String obj)
      A static utility method.
      Parameters:
      obj - A String.
      Returns:
      true if obj is a SUO-KIF logical quantifier, else false.

    • isCommutative

      public static boolean isCommutative(String obj)
      A static utility method.
      Parameters:
      obj - Presumably, a String.
      Returns:
      true if obj is a SUO-KIF commutative logical operator, else false.

    • formatWikipedia

      public String formatWikipedia(String documentation)
      Hyperlink "[from Wikipedia]" if it occurs

    • formatDocumentation

      public String formatDocumentation(String href, String documentation, String language)
      Hyperlink terms identified with 'invalid input: '&'%' to the URL that brings up that term in the browser. Handle (and ignore) suffixes on the term. For example "invalid input: '&'%Processes" would get properly linked to the term "Process", if present in the knowledge base.

    • formatStaticDocumentation

      public String formatStaticDocumentation(String documentation, String language, boolean onePage)
      Hyperlink terms identified with 'invalid input: '&'%' to the URL that brings up that term in the ba static file Handle (and ignore) suffixes on the term. For example "invalid input: '&'%Processes" would get properly linked to the term "Process", if present in the knowledge base.

    • writeInferenceEngineFormulas

      public String writeInferenceEngineFormulas(Set<String> forms)
      Save the contents of the current KB to a file.

    • createInferenceEngine

      public InferenceEngine createInferenceEngine(InferenceEngine.EngineFactory factory)
      Creates InferenceEngine and loads all of the constituents into it.
      Parameters:
      factory - Factory object used to create new InferenceEngine.
      Returns:
      InferenceEngine object with all constituents loaded.

    • loadVampire

      public void loadVampire()
      Checks for a Vampire executable, preprocesses all of the constituents. This no-arg version reads from the static SUMOKBtoTPTPKB.lang field. For thread-safe operation during background TPTP generation, use loadVampire(String requestedLang) instead.

    • loadVampire

      public void loadVampire(String requestedLang)
      Checks for a Vampire executable, preprocesses all of the constituents. This version takes the requested language as a parameter to avoid race conditions with background TPTP generation threads that modify the static SUMOKBtoTPTPKB.lang field.
      Parameters:
      requestedLang - The TPTP language format requested by the user ("fof" or "tff")

    • loadLeo

      public void loadLeo()
      Checks for a Leo executable, preprocesses all of the constituents. This no-arg version reads from the static SUMOKBtoTPTPKB.lang field.

    • loadLeo

      public void loadLeo(String requestedLang)
      Checks for a Leo executable, preprocesses all of the constituents. This version takes the requested language as a parameter to avoid race conditions with background TPTP generation threads.
      Parameters:
      requestedLang - The TPTP language format requested by the user ("fof" or "tff")

    • loadEProver

      public void loadEProver()
      Starts EProver and collects, preprocesses and loads all of the constituents into it. This no-arg version reads from the static SUMOKBtoTPTPKB.lang field. For thread-safe operation during background TPTP generation, use loadEProver(String requestedLang) instead.

    • loadEProver

      public void loadEProver(String requestedLang)
      Starts EProver and collects, preprocesses and loads all of the constituents into it. This version takes the requested language as a parameter to avoid race conditions with background TPTP generation threads that modify the static SUMOKBtoTPTPKB.lang field.
      Parameters:
      requestedLang - The TPTP language format requested by the user ("fof" or "tff")

    • preProcess

      public Set<String> preProcess(Set<String> forms)
      Preprocess the knowledge base to TPTP. This includes "holds" prefixing, ticking nested formulas, expanding row variables, and translating mathematical relation operators. All the real work is done in Formula.preProcess().
      Returns:
      a TreeSet of Strings.

    • getLoadFormatMapsAttempted

      public List<String> getLoadFormatMapsAttempted()
      Returns:
      a defensive copy of loadFormatMapsAttempted.

    • getSortedTermFrequency

      public List<com.articulate.sigma.utils.Pair> getSortedTermFrequency()

    • runProver

      public TPTP3ProofProcessor runProver(String[] args, int timeout)

    • addToAxiomCount

      public static void addToAxiomCount(Map<String,Integer> currentCount, Set<String> newAxioms)
      Keep a count of axioms

    • addTermFormat

      public void addTermFormat(String lang, String term, String format)
      add to term format map HashMapinvalid input: '<'String, HashMapinvalid input: '<'String, String>>();

    • collectSourceAxioms

      public static Map<String,Formula> collectSourceAxioms(KB kb, TPTP3ProofProcessor tpp)
      Attempt to provide guidance on the likely cause of a contradiction by removing the axioms involved in a contradiction one-by-one and trying again. @see contradictionHelp()

    • countUserAssertionFormulasInMemory

      public int countUserAssertionFormulasInMemory()
      Count how many Formula objects currently in memory came from the per-test user assertions file (e.g. SUMO_UserAssertions.kif).

    • purgeUserAssertionsFromMemory

      public int purgeUserAssertionsFromMemory()
      Remove all formulas in memory whose sourceFile is _UserAssertions.kif. Returns how many formulas were removed from formulaMap.

    • contradictionHelp

      public static void contradictionHelp(KB kb, String[] args, int timeout)
      Attempt to provide guidance on the likely cause of a contradiction by removing the axioms involved in a contradiction one-by-one and trying again.

    • test

      public static void test()

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • showHelp

      public static void showHelp()

    • main

      public static void main(String[] args) throws IOException
      Command line entry point for this class
      Parameters:
      args - command line arguments (examples from showHelp)
      Throws:
      IOException