com.articulate.sigma.trans

Class TPTP3ProofProcessor

java.lang.Object

com.articulate.sigma.trans.TPTP3ProofProcessor

public class TPTP3ProofProcessor
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
java.util.ArrayList<java.lang.String>	bindings
java.util.ArrayList<ProofStep>	proof
java.lang.String	status

Constructor Summary

Constructors

Constructor and Description
TPTP3ProofProcessor()

Method Summary

Modifier and Type	Method and Description
static void	findTypesForSkolemTerms(TPTP3ProofProcessor tpp, KB kb) Return the most specific type for skolem variable.
java.lang.String	getInferenceType(java.lang.String supportId)
static void	main(java.lang.String[] args)
static java.util.ArrayList<java.lang.String>	parseAnswerTuples(java.lang.String st, KB kb, FormulaPreprocessor fp) Return a list of answers if E finds bindings for wh- queries.
java.util.ArrayList<java.lang.Integer>	parseInferenceObject(java.lang.String supportId)
static TPTP3ProofProcessor	parseProofOutput(java.util.ArrayList<java.lang.String> lines, KB kb) Compute binding and proof from E's response
static TPTP3ProofProcessor	parseProofOutput(java.io.LineNumberReader lnr, KB kb) Compute bindings and proof from E's response
static TPTP3ProofProcessor	parseProofOutput(java.lang.String st, KB kb)
ProofStep	parseProofStep(java.lang.String line) Parse a step like the following into its constituents fof(c_0_5, axiom, (s__subclass(s__Artifact,s__Object)), c_0_3).
java.util.ArrayList<java.lang.Integer>	parseSupports(java.lang.String supportId) Parse support / proof statements in E's response
void	printAnswers() Print out E's bindings
void	processAnswers(java.lang.String line) Return bindings from E's answer tuples
static void	testE()
static void	testParseProofFile()
static void	testParseProofStep()
java.lang.String	toString() Convert bindings in list to string
static java.lang.String	trimBrackets(java.lang.String line) Remove brackets if it contains
static java.lang.String	trimParens(java.lang.String line) Remove parentheses if it contains

Methods inherited from class java.lang.Object

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

Field Detail

status

public java.lang.String status

bindings

public java.util.ArrayList<java.lang.String> bindings

proof

public java.util.ArrayList<ProofStep> proof

Constructor Detail

TPTP3ProofProcessor

public TPTP3ProofProcessor()

Method Detail

toString

public java.lang.String toString()

Convert bindings in list to string

Overrides:

toString in class java.lang.Object

trimBrackets

public static java.lang.String trimBrackets(java.lang.String line)

Remove brackets if it contains

trimParens

public static java.lang.String trimParens(java.lang.String line)

Remove parentheses if it contains

parseInferenceObject

public java.util.ArrayList<java.lang.Integer> parseInferenceObject(java.lang.String supportId)

getInferenceType

public java.lang.String getInferenceType(java.lang.String supportId)

parseSupports

public java.util.ArrayList<java.lang.Integer> parseSupports(java.lang.String supportId)

Parse support / proof statements in E's response

parseProofStep

public ProofStep parseProofStep(java.lang.String line)

Parse a step like the following into its constituents fof(c_0_5, axiom, (s__subclass(s__Artifact,s__Object)), c_0_3). fof(c_0_2, negated_conjecture, (~(?[X1]:(s__subclass(X1,s__Object)&~$answer(esk1_1(X1))))), inference(assume_negation,[status(cth)],[inference(add_answer_literal,[status(thm)],[c_0_0, theory(answers)])])).

processAnswers

public void processAnswers(java.lang.String line)

Return bindings from E's answer tuples

findTypesForSkolemTerms

public static void findTypesForSkolemTerms(TPTP3ProofProcessor tpp,
                                           KB kb)

Return the most specific type for skolem variable.

Parameters:

tpp - The structure learned from E's response

kb - The knowledge base used to find skolem term's types For example, original binding = esk3_0 set binding = "An instance of Human" (Human is the most specific type for esk3_0 in the given proof) original binding = esk3_1 set binding = "An instance of Human, Agent" (If multiple types are found for esk3_1)

printAnswers

public void printAnswers()

Print out E's bindings

parseProofOutput

public static TPTP3ProofProcessor parseProofOutput(java.io.LineNumberReader lnr,
                                                   KB kb)

Compute bindings and proof from E's response

parseProofOutput

public static TPTP3ProofProcessor parseProofOutput(java.util.ArrayList<java.lang.String> lines,
                                                   KB kb)

Compute binding and proof from E's response

parseAnswerTuples

public static java.util.ArrayList<java.lang.String> parseAnswerTuples(java.lang.String st,
                                                                      KB kb,
                                                                      FormulaPreprocessor fp)

Return a list of answers if E finds bindings for wh- queries. Return "Proof Found" if E finds contradiction for boolean queries. For example, tuple_list = [[esk3_1(s__Org1_1)]|_] Output = [Org1_1] tuple_list = [[esk3_0]|_] Output = [An instance of Human] (Human is the most specific type for esk3_0 in the given proof)

parseProofOutput

public static TPTP3ProofProcessor parseProofOutput(java.lang.String st,
                                                   KB kb)

testParseProofFile

public static void testParseProofFile()

testE

public static void testE()

testParseProofStep

public static void testParseProofStep()

main

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