Package com.articulate.sigma.trans

Class SUMOtoTFAform

java.lang.Object
com.articulate.sigma.trans.SUMOtoTFAform
public class SUMOtoTFAform extends Object
Created by apease on 7/23/18.

  • Field Details

    • kb

      public static KB kb

    • debug

      public static boolean debug

    • varmap

      public static Map<String,Set<String>> varmap

    • initialized

      public static boolean initialized

    • fp

      public static FormulaPreprocessor fp

    • numericConstraints

      public static Map<String,String> numericConstraints

    • numericVars

      public static Map<String,String> numericVars

    • numConstAxioms

      public static Set<String> numConstAxioms

    • numericConstantTypes

      public static Map<String,String> numericConstantTypes

    • numericConstantValues

      public static Map<String,String> numericConstantValues

    • numericConstantCount

      public static int numericConstantCount

    • filterMessage

      public static String filterMessage

    • sorts

      public Set<String> sorts

    • errors

      public static Set<String> errors

  • Constructor Details

    • SUMOtoTFAform

      public SUMOtoTFAform()

  • Method Details

    • isComparisonOperator

      public static boolean isComparisonOperator(String s)
      comparison ops are EQUAL, GT, GTET, LT, LTET

    • isMathFunction

      public static boolean isMathFunction(String s)
      math ops are PLUSFN, MINUSFN, TIMESFN, DIVIDEFN, FLOORFN, RemainderFn, CeilingFn, RoundFn

    • isEqualTypeOp

      public static boolean isEqualTypeOp(String s)

    • withoutSuffix

      public static String withoutSuffix(String s)

    • setNumericFunctionInfo

      public static void setNumericFunctionInfo()
      Set the cached information of automatically generated functions and relations needed to cover the polymorphic type signatures of build-in TFF terms

    • fill

      public static void fill(List<String> ar, int start, int end)
      Fill the indicated elements with "Entity", starting at start and ending at end-1

    • fill

      public static void fill(List<String> ar, int start, int end, String fillStr)
      Fill the indicated elements with the given string, starting at start and ending at end-1

    • safeSet

      public static void safeSet(List<String> ar, int index, String val)
      If there's no such element index, fill the previous elements with Entity

    • relationExtractNonNumericSig

      protected static List<String> relationExtractNonNumericSig(String rel)
      Return the full signature

    • relationExtractSigFromName

      public static List<String> relationExtractSigFromName(String rel)
      Extract modifications to the relation signature from annotations embedded in the suffixes to its name. Note that the first argument to a relation is number 1, so getting the 0th argument of the returned ArrayList would give an empty string result for a relation.

    • relationExtractUpdateSigFromName

      public static List<String> relationExtractUpdateSigFromName(String rel)
      Extract modifications to the relation signature from annotations embedded in the suffixes to its name. Note that the first argument to a relation is number 1, so getting the 0th argument of the returned ArrayList would give an empty string result for a relation.

    • getBareTerm

      public static String getBareTerm(String s)
      Get just the bare SUMO term without prefixes or suffixes

    • hasNumericSuper

      public static boolean hasNumericSuper(List<String> argTypes)
      The arg type list requires expansion since it contains a superclass of Integer, and therefore could be used with more than one TF) numerical type.

    • findType

      public static String findType(Formula f)
      Returns:
      the TF0-relevant type of the term whether it's a literal number, variable with a numeric type or function

    • isNumeric

      public static boolean isNumeric(Formula f)
      a number, a variable with a numeric type or a function symbol or function with a numeric type

    • isNumericType

      public static boolean isNumericType(String s)

    • isBuiltInNumericType

      public static boolean isBuiltInNumericType(String s)

    • hasNumeric

      public static boolean hasNumeric(List<String> argTypes)
      Check if at least one of the types in the list is a numeric type

    • equalTFFsig

      public static boolean equalTFFsig(List<String> argTypes1, List<String> argTypes2, String pred)
      Check if type signatures of SUMO would be equivalent TFF signatures.
      Parameters:
      pred - is used just to give a meaningful error message

    • numTypePromotion

      public static String numTypePromotion(Formula f, String parentType)
      if the formula is a numeric atom or variable or a function with a number range and that type is more specific that the parentType, promote it with $to_real or invalid input: '&to_rat'
      Returns:
      promotion function call with learning parent, or null otherwise

    • processRecurse

      public static String processRecurse(Formula f, String parentType)
      process a formula into TF0
      Parameters:
      f - the formula to process
      parentType - is the type restriction that applies to this formula, if it's part of a larger formula

    • composeSuffix

      protected static String composeSuffix(String op, String suffix)
      if the operator already has a suffix, revise it with the new suffix in the case where the new argument type is more specific

    • mostSpecificType

      public static String mostSpecificType(Collection<String> args)
      Create a specialized version of KB.mostSpecificTerm() that biases the results for TFF. Prefer a built-in numeric type (equivalents to $int, $rat, $real) over any more specific type in SUMO

    • promoteToBuiltIn

      public static String promoteToBuiltIn(String t)
      Promote type to the most specific number that is a TFF type or superclass

    • constrainPair

      public static String constrainPair(String t1, String t2)
      Pick the most specific number type that is a TFF type or superclass

    • bestOfPair

      public static String bestOfPair(String t1, String t2)
      Pick the most general number among two numbers or the most specific term otherwise

    • constrainTerm

      public static String constrainTerm(String t1, String t2)
      Constrain a type based on a second type. If the second type is built-in type and first is not, pick the built-in type. If the second type and first type are both built-in types, pick the more specific. If the second type is more general than the first, throw an error.

    • mostSpecificSignature

      public static List<String> mostSpecificSignature(List<String> args1, List<String> args2)
      Find the most specific TFF type or superclass at every argument position

    • bestSignature

      public static List<String> bestSignature(List<String> args1, List<String> args2)
      Find the best type at every argument position

    • mostSpecificTFFTerm

      public static String mostSpecificTFFTerm(Collection<String> args)
      Create a specialized version of KB.mostSpecificTerm() that biases the results for TFF. Prefer the most specific type but no subclasses of a built-in numeric type (equivalents to $int, $rat, $real)

    • bestSpecificTerm

      public static String bestSpecificTerm(Collection<String> args)
      Create a specialized version of KB.mostSpecificTerm() that biases the results for TFF. Prefer a built-in numeric type (equivalents to $int, $rat, $real) over any more specific type in SUMO. Prefer the most general numeric type.

    • elimUnitaryLogops

      public static String elimUnitaryLogops(Formula f)
      Recursive routine to eliminate occurrences of 'forall', 'exists', 'invalid input: '<'=>', '=>', 'and', 'xor' and 'or' that have only one or zero arguments
      Returns:
      the corrected formula as a string

    • instantiateNumericConstants

      public static Formula instantiateNumericConstants(Formula f)
      Substitute the values of numeric constants for their names. Note that this is risky since it must be kept up to date with the content of the knowledge base. TODO: generalize this

    • removeNumericInstance

      public static String removeNumericInstance(String s)
      When predicate variable substitution occurs it can result in an argument to the predicate being defined as a particular type. If that type is numeric, it will conflict with TFF's built in types and need to be removed, since the type will be specified in the quantifier list, albeit with a constraint from the numericConstraints list if the type is not a TFF fundamental type of $int, $rat, or $real

    • inconsistentVarTypes

      public static boolean inconsistentVarTypes()
      Check whether variables have multiple mutually exclusive types

    • typeConflict

      public static boolean typeConflict(Formula f)
      Reject formulas that wind up with type conflicts despite all attempts to resolve them

    • sortFromRelation

      public static String sortFromRelation(String rel)
      Create a sort spec from the relation name with embedded types

    • missingSorts

      public Set<String> missingSorts(Formula f)
      Returns:
      a list of TFF relation sort definitions to cover ListFn statements that have diverse sorts

    • process

      public static String process(Formula f, boolean query)
      This is the primary method of the class. It takes a SUO-KIF formula and returns a TFF formula.

    • process

      public static String process(String suoString, boolean query)
      Parse a single formula into TPTP format.
      Parameters:
      suoString - the formula entry to parse
      query - true if the suoString is a query

    • processList

      public static Collection<String> processList(Collection<Formula> l)

    • modifyPrecond

      protected static String modifyPrecond(Formula f)
      remove statements of the form (instance ?X term) if 'term' is Integer or RealNumber and ?X is already of that type in the quantifier list for the formula
      Returns:
      the modified formula

    • modifyTypesToConstraints

      protected static String modifyTypesToConstraints(Formula f)
      replace type statements of the form (instance ?X term), where term is a subtype of Integer or RealNumber with a constraint that defines that type
      Returns:
      String version of the modified formula

    • initNumericConstantTypes

      public static void initNumericConstantTypes()

    • initOnce

      public static void initOnce()

    • test1

      public static void test1()

    • test2

      public static void test2()

    • test3

      public static void test3()

    • test4

      public static void test4()

    • test5

      public static void test5()

    • test6

      public static void test6()

    • test7

      public static void test7()

    • test8

      public static void test8()

    • test9

      public static void test9()

    • test10

      public static void test10()

    • testRelEmbed

      public static void testRelEmbed()

    • testRelExtract

      public static void testRelExtract()

    • testCourse

      public static void testCourse()

    • showHelp

      public static void showHelp()

    • main

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