Class FormulaPreprocessor

java.lang.Object
com.articulate.sigma.FormulaPreprocessor

public class FormulaPreprocessor extends Object
  • Field Details

    • debug

      public static boolean debug
    • addOnlyNonNumericTypes

      public static boolean addOnlyNonNumericTypes
    • errors

      public static Set<String> errors
  • Constructor Details

    • FormulaPreprocessor

      public FormulaPreprocessor()
  • Method Details

    • findType

      public static String findType(int numarg, String pred, KB kb)
      Find the argument type restriction for a given predicate and argument number that is inherited from one of its super-relations. A "+" is appended to the type if the parameter must be a class, meaning that a domainSubclass is defined for this argument in one of the loaded .kif files. Argument number 0 is used for the return type of a Function. Asking for a non-existent arg will return null;
    • winnowTypeList

      public void winnowTypeList(Set<String> types, KB kb)
      This method tries to remove all but the most specific relevant classes from a List of sortal classes.
      Parameters:
      types - A List of classes (class name Strings) that constrain the value of a SUO-KIF variable.
      kb - The KB used to determine if any of the classes in the List types are redundant.
    • findTypeRestrictions

      public Map<String,Set<String>> findTypeRestrictions(Formula form, KB kb)
      Find all the type restrictions on the variables in a formula, including constraints from relation argument typing as well as explicitly stated types from instance and subclass expressions.
    • findAllTypeRestrictions

      public Map<String,Set<String>> findAllTypeRestrictions(Formula form, KB kb)
    • addTypeRestrictions

      public Formula addTypeRestrictions(Formula form, KB kb)
      Add clauses for every variable in the antecedent to restrict its type to the type restrictions defined on every relation in which it appears. For example (=> (foo ?A B) (bar B ?A)) (domain foo 1 Z) would result in (=> (instance ?A Z) (=> (foo ?A B) (bar B ?A)))
    • getMostRelevantType

      protected String getMostRelevantType(KB kb, Set<String> types)
      Get the most specific type for variables.
      Parameters:
      kb - The KB to be used for processing
      types - a list of sumo types for a sumo term/variable
      Returns:
      the most specific sumo type for the term/variable For example types of ?Writing = [Entity, Physical, Process, IntentionalProcess, ContentDevelopment, Writing] return the most specific type Writing
    • findExplicitTypesInAntecedent

      public Map<String,Set<String>> findExplicitTypesInAntecedent(KB kb, Formula form)
      Collect the types of any variables that are specifically defined in the antecedent of a rule with an instance or subclass expression. TODO: This may ultimately require CNF conversion and then checking negative literals, but for now it's just a hack to grab preconditions.
    • findExplicitTypesClassesInAntecedent

      public Map<String,Set<String>> findExplicitTypesClassesInAntecedent(KB kb, Formula form)
      Collect the types of any variables that are specifically defined in the antecedent of a rule with an instance expression; Collect the super classes of any variables that are specifically defined in the antecedent of a rule with an subclass expression;
    • findExplicitTypes

      public Map<String,Set<String>> findExplicitTypes(KB kb, Formula form)
      Collect variable names and their types from instance or subclass expressions. subclass restrictions are marked with a '+'.
      Parameters:
      form - The formula in KIF syntax
      Returns:
      A map of variables paired with a set of sumo types collected from instance and subclass expressions. TODO: This may ultimately require CNF conversion and then checking negative literals, but for now it's just a hack to grab preconditions.
    • findExplicitTypesClasses

      public void findExplicitTypesClasses(KB kb, Formula form, Map<String,Set<String>> varExplicitTypes, Map<String,Set<String>> varExplicitClasses)
      Collect variable names and their types from instance or subclass expressions.
      Parameters:
      form - The formula in KIF syntax
      varExplicitTypes - A map of variables paired with sumo types collected from instance expressions
      varExplicitClasses - A map of variables paired with sumo types collected from subclass expression
    • findExplicitTypesRecurse

      public static void findExplicitTypesRecurse(KB kb, Formula form, boolean isNegativeLiteral, Map<String,Set<String>> varExplicitTypes, Map<String,Set<String>> varExplicitClasses)
      Recursively collect a variable name and its types.
    • computeVariableTypes

      public Map<String,Set<String>> computeVariableTypes(Formula form, KB kb)
      This method returns a HashMap that maps each String variable in this the names of types (classes) of which the variable must be an instance or the names of types of which the variable must be a subclass. Note that this method does not capture explicit type from assertions such as (=> (instance ?Foo Bar) ...). This method just consider restrictions implicitly defined from the arg types of relations.
      Parameters:
      kb - The KB to be used to compute the sortal constraints for each variable.
      Returns:
      A HashMap of variable names and their types. Subclass restrictions are marked with a '+', meaning that a domainSubclass is defined for this argument in one of the loaded .kif files. Instance restrictions have no special mark.
    • replacePredVarsAndRowVars

      protected List<Formula> replacePredVarsAndRowVars(Formula form, KB kb, boolean addHoldsPrefix)
      Tries to successively instantiate predicate variables and then expand row variables in this Formula, looping until no new Formulae are generated.
      Parameters:
      kb - The KB to be used for processing this Formula
      addHoldsPrefix - If true, predicate variables are not instantiated
      Returns:
      an ArrayList of Formula(s), which could be empty.
    • preProcess

      public Set<Formula> preProcess(Formula form, boolean isQuery, KB kb)
      Pre-process a formula before sending it to the theorem prover. This includes ignoring meta-knowledge like documentation strings, translating mathematical operators, quoting higher-order formulas, expanding row variables and instantiating predicate variables
      Parameters:
      form - a formula to process
      isQuery - If true the Formula is a query and should be existentially quantified, else the Formula is a statement and should be universally quantified
      kb - The KB to be used for processing this Formula
      Returns:
      an Set of Formula(s), which could be empty.
    • testFindTypes

      public static void testFindTypes()
    • testFindExplicit

      public static void testFindExplicit()
    • testAddTypes

      public static void testAddTypes()
    • testOne

      public static void testOne()
    • testTwo

      public static void testTwo()
    • testThree

      public static void testThree()
    • testFour

      public static void testFour()
    • testFive

      public static void testFive()
    • test6

      public static void test6()
    • main

      public static void main(String[] args)