Package com.articulate.sigma.trans

Class THFnew

java.lang.Object
com.articulate.sigma.trans.THFnew
public class THFnew extends Object

  • Field Details

    • debug

      public static boolean debug

    • axNum

      public static int axNum

    • badUsageSymbols

      public static Set<Formula> badUsageSymbols

    • predicateTerms

      public static Set<String> predicateTerms

  • Constructor Details

    • THFnew

      public THFnew()

  • Method Details

    • processLogOp

      public static String processLogOp(Formula f, Formula car, List<String> args, Map<String,Set<String>> typeMap)

    • processEquals

      public static String processEquals(Formula f, Formula car, List<String> args, Map<String,Set<String>> typeMap)

    • processRecurse

      public static String processRecurse(Formula f, Map<String,Set<String>> typeMap)

    • getTHFtype

      public static String getTHFtype(String v, Map<String,Set<String>> typeMap)
      Map a KIF variable to a THF type, based on its inferred SUMO types. - Formula variables become (w > $o) so they can be applied as F @ W. - World variables become w. - Modal variables become m. - Everything else collapses to $i.

    • generateQList

      public static String generateQList(Formula f, Map<String,Set<String>> typeMap, Set<String> vars)

    • generateQListNonModal

      public static String generateQListNonModal(Formula f, Map<String,Set<String>> typeMap, Set<String> vars)

    • process

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

    • processNonModal

      public static String processNonModal(Formula f, Map<String,Set<String>> typeMap, boolean query)

    • variableArity

      public static boolean variableArity(KB kb, String pred)

    • adjustArity

      public static Formula adjustArity(KB kb, Formula f)
      Adding the world argument messes up pre-processing for variable arity relations, so we have to decrement the numerical suffix as a hack. (s__partition__4 @ s__PsychologicalAttribute @ s__StateOfMind @ s__TraitAttribute @ V__W1) ) needs to be s__partition__3

    • makeWorldVar

      public static String makeWorldVar(KB kb, Formula f)

    • oneTrans

      public static void oneTrans(KB kb, Formula f, PrintWriter bw) throws IOException
      Throws:
      IOException

    • oneTransNonModal

      public static void oneTransNonModal(KB kb, Formula f, Writer bw) throws IOException
      Throws:
      IOException

    • protectedRelation

      public static boolean protectedRelation(String s)

    • exclude

      public static boolean exclude(Formula f, KB kb, Writer out) throws IOException
      Decide whether to exclude a formula from THF export. This filter: - removes unsupported syntactic constructs (quotes, $true/$false), - removes meta-logical axioms about the class Formula and bare variables in formula position, - enforces constraints on how modal/HOL symbols may be used (never as ordinary individuals in non-modal heads), - drops a small set of known-bad SUMO terms (problematic_terms). NOTE: Pure arithmetic functions such as AdditionFn, MultiplicationFn, LogFn, SquareRootFn, etc. are NOT excluded here. They are treated as world-free functions and handled via THFnew's type system.
      Throws:
      IOException

    • excludePred

      public static boolean excludePred(String pred, Writer out) throws IOException
      Predicates that denote formulas that shouldn't be included in the translation.
      Throws:
      IOException

    • excludeForTypedef

      public static boolean excludeForTypedef(String pred, Writer out) throws IOException
      Predicates that denote formulas that shouldn't be included in type definitions of the translation.
      Throws:
      IOException

    • sigString

      public static String sigString(String functor, List<String> sig, KB kb, boolean function)
      Build a THF type string from a SUMO signature.
      Parameters:
      functor - the predicate / function symbol whose type we build
      sig - the list of SUMO argument/result types (as strings)
      kb - the KB, used for isInstanceOf checks
      function - true if this is a function symbol (first entry in sig is range) NOTE: - For "modal" predicates in Modals.formulaPreds / regHOLpred we treat Formula arguments as (w > $o) (e.g. confersObligation, desires, ...). - KappaFn is a special case: although it appears in formulaPreds, in the existing SUMO axioms its Formula argument is used as a *plain* proposition (already world-instantiated), so we type that argument as $o instead.

    • sigStringNonModal

      public static String sigStringNonModal(String pred, List<String> sig, KB kb, boolean function)

    • writeIntegerTypes

      public static void writeIntegerTypes(KB kb, Writer out) throws IOException
      Throws:
      IOException

    • writeTypes

      public static void writeTypes(KB kb, Writer out) throws IOException
      Throws:
      IOException

    • writeTypesNonModal

      public static void writeTypesNonModal(KB kb, Writer out) throws IOException
      Throws:
      IOException

    • analyzeBadUsages

      public static void analyzeBadUsages(KB kb)

    • transModalTHF

      public static void transModalTHF(KB kb)

    • transPlainTHF

      public static void transPlainTHF(KB kb)

    • excludeNonModal

      public static boolean excludeNonModal(Formula f, KB kb, Writer out) throws IOException
      Throws:
      IOException

    • test

      public static void test(KB kb)

    • showHelp

      public static void showHelp()

    • main

      public static void main(String[] args)