com.articulate.sigma

Class ProofProcessor

java.lang.Object

com.articulate.sigma.ProofProcessor

public class ProofProcessor
extends java.lang.Object

Process results from the inference engine.

Constructor Summary

Constructors

Constructor and Description
ProofProcessor(java.util.ArrayList<BasicXMLelement> xmlInput) Take an ArrayList of BasicXMLelement (s) and process them as needed

Method Summary

Modifier and Type	Method and Description
boolean	equalsAnswer(int answerNum, java.lang.String expectedAnswer) Compare the answer with the expected answer.
static void	main(java.lang.String[] args) A main method, used only for testing.
int	numAnswers() Return the number of answers contained in this proof.
static java.lang.String	removeNestedAnswerClause(java.lang.String st) Remove the $answer clause that eProver returns, including any surrounding connective.
static java.util.ArrayList<java.lang.String>	returnSkolemStmt(java.lang.String skolem, java.util.ArrayList<ProofStep> proofSteps) Looks for skolem function from proofsteps if query is not given.
static void	tallyAxioms(java.lang.String file) Tally the number of appearances of a particular axiom label in a file.
static void	testFormatProof()
static void	testRemoveAnswer()
static java.lang.String	tptpProof(java.util.ArrayList<ProofStep> proofSteps) Convert XML proof to TPTP format

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ProofProcessor

public ProofProcessor(java.util.ArrayList<BasicXMLelement> xmlInput)

Take an ArrayList of BasicXMLelement (s) and process them as needed

Method Detail

equalsAnswer

public boolean equalsAnswer(int answerNum,
                            java.lang.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 java.util.ArrayList<java.lang.String> returnSkolemStmt(java.lang.String skolem,
                                                                     java.util.ArrayList<ProofStep> 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 java.lang.String removeNestedAnswerClause(java.lang.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 java.lang.String tptpProof(java.util.ArrayList<ProofStep> proofSteps)

Convert XML proof to TPTP format

testRemoveAnswer

public static void testRemoveAnswer()

tallyAxioms

public static void tallyAxioms(java.lang.String file)

Tally the number of appearances of a particular axiom label in a file. This is intended to be used to analyse 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()

main

public static void main(java.lang.String[] args)

A main method, used only for testing. It should not be called during normal operation.