Package com.articulate.sigma

Class ProofProcessor

java.lang.Object
com.articulate.sigma.ProofProcessor
public class ProofProcessor extends Object
Process results from the inference engine.

  • Constructor Details

    • ProofProcessor

      public ProofProcessor(List<BasicXMLelement> xmlInput)
      Take an ArrayList of BasicXMLelement (s) and process them as needed

  • Method Details

    • equalsAnswer

      public boolean equalsAnswer(int answerNum, String expectedAnswer)
      Compare the answer with the expected answer. Note that this method is very unforgiving in that it requires the exact same format for the expected answer, including the order of variables.

    • returnSkolemStmt

      public static List<String> returnSkolemStmt(String skolem, List<tptp_parser.TPTPFormula> proofSteps)
      Looks for skolem function from proofsteps if query is not given. There are two types of skolem functions: one with arguments, for instance: (sk0 Human123) or one without, for example: sk2 We need to find either of these in the proofs to see what relationship it goes into

    • removeNestedAnswerClause

      public static String removeNestedAnswerClause(String st)
      Remove the $answer clause that eProver returns, including any surrounding connective.

    • numAnswers

      public int numAnswers()
      Return the number of answers contained in this proof.

    • tptpProof

      public static String tptpProof(List<ProofStep> proofSteps)
      Convert XML proof to TPTP format

    • testRemoveAnswer

      public static void testRemoveAnswer()

    • tallyAxioms

      public static void tallyAxioms(String file)
      ************************************************************** Tally the number of appearances of a particular axiom label in a file. This is intended to be used to analyze E output that looks for contradictions, with the intuition that axioms that appear in most or all of the contractions found are the source of the problem.

    • testFormatProof

      public static void testFormatProof()

    • testFormatProof2

      public static void testFormatProof2(String filename)

    • showHelp

      public static void showHelp()

    • main

      public static void main(String[] args)
      A main method, used only for testing. It should not be called during normal operation.