Package com.articulate.sigma.trans

Class TPTPutil

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

  • Constructor Details

    • TPTPutil

      public TPTPutil()

  • Method Details

    • htmlTPTPFormat

      public static String htmlTPTPFormat(Formula f, String hyperlink, boolean traditionalLogic)
      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.

    • htmlizeSUMOTFA

      public static String htmlizeSUMOTFA(String tfa, String hyperlink)
      Take a plain SUMOtoTFAform string and wrap every s__ token in a hyperlink, similar to htmlTPTPFormat().
      Parameters:
      tfa - the raw SUMOtoTFAform string
      hyperlink - the base URL (e.g. "http://sigma.ontologyportal.org:4040/sigma?kb=SUMOinvalid input: '&term'=")
      Returns:
      HTML-formatted string with linked terms

    • sourceAxiom

      public static boolean sourceAxiom(tptp_parser.TPTPFormula ps)
      Is the axiom in a proof a source authored axiom from SUMO, rather than one automatically derived or introduced by a theorem prover

    • citation

      public static boolean citation(String sumoStep, String stepName, KB kb)
      Is there a citation as a containsFormula relation for this axiom?

    • getCitationString

      public static String getCitationString(String sumoStep, String stepName, KB kb)
      Is there a citation as a containsFormula relation for this axiom?

    • test

      public static void test()

    • clearProofFile

      public static List<String> clearProofFile(List<String> lines)
      Cleans and normalizes the contents of a TPTP proof file. Steps performed: 1. Keeps comment lines ("%") that appear before the first fof(...) line and after the last one. 2. Merges multi-line fof(...) formulas into single lines by concatenating their continuation lines until a closing ")." is found. 3. Returns a cleaned version of the proof containing: - Header comments - All compacted fof(...) lines - Footer comments

    • dropOnePremiseFormulasFOF

      public static List<String> dropOnePremiseFormulasFOF(List<String> proofLines)
      Processes a TPTP proof file and removes all proof steps that have only a single premise (e.g., trivial inferences or direct copies). Steps performed: 1. Initializes the Sigma knowledge base (KBmanager) to ensure ontology data is loaded. 2. Cleans the raw proof lines using clearProofFile(), preserving only header/footer comments and merging multi-line fof(...) entries into single lines. 3. Parses the proof output into structured TPTPFormula objects. 4. Calls simplifyProof(1) to remove all single-premise proof steps. 5. Renumbers the remaining proof steps to maintain consistent references. 6. Reconstructs the proof by: - Keeping the original header and footer comments. - Converting each remaining TPTPFormula back into fof(...) format. - Combining them into a normalized list of proof lines. Returns a cleaned proof where all trivial one-premise derivations are dropped, maintaining logical consistency and readability.

    • replaceFOFinfRule

      public static List<String> replaceFOFinfRule(List<String> proofLines, List<tptp_parser.TPTPFormula> authored_lines)

    • writeMinTPTP

      public static List<tptp_parser.TPTPFormula> writeMinTPTP(List<tptp_parser.TPTPFormula> proof)

    • processProofLines

      public static List<tptp_parser.TPTPFormula> processProofLines(List<String> inputLines)

    • extractIncludesFromTPTP

      public static List<String> extractIncludesFromTPTP(File tptpFile)

    • validateIncludesInTPTPFiles

      public static String validateIncludesInTPTPFiles(List<String> includes, String includesPath)

    • showHelp

      public static void showHelp()

    • main

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