com.articulate.sigma

Class ProofProcessor

java.lang.Object

com.articulate.sigma.ProofProcessor

public class ProofProcessor
extends Object

Process results from the inference engine.

Constructor Summary

Constructors

Constructor and Description
ProofProcessor(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, String expectedAnswer) Compare the answer with the expected answer.
static void	main(String[] args) A main method, used only for testing.
int	numAnswers() Return the number of answers contained in this proof.
static String	removeNestedAnswerClause(String st) Remove the $answer clause that eProver returns, including any surrounding connective.
static ArrayList<String>	returnSkolemStmt(String skolem, ArrayList<ProofStep> proofSteps) Looks for skolem function from proofsteps if query is not given.
static void	testFormatProof()
static void	testRemoveAnswer()
static String	tptpProof(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(ArrayList<BasicXMLelement> xmlInput)

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

Method Detail

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 ArrayList<String> returnSkolemStmt(String skolem,
                                                 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 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(ArrayList<ProofStep> proofSteps)

Convert XML proof to TPTP format

testRemoveAnswer

public static void testRemoveAnswer()

testFormatProof

public static void testFormatProof()

main

public static void main(String[] args)

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