java.lang.Object

com.articulate.sigma.trans.TPTP3ProofProcessor

public class TPTP3ProofProcessor extends Object

Nested Class Summary

Nested Classes

Modifier and Type

Class

Description

static enum

TPTP3ProofProcessor.GraphFormulaFormat
Field Summary

Fields

Modifier and Type

Field

Description

Map<String,String>

bindingMap

List<String>

bindings

boolean

containsFalse

static boolean

debug

Map<String,Integer>

idTable

boolean

inconsistency

boolean

noConjecture

List<tptp_parser.TPTPFormula>

proof

Map<String,String>

skolemTypes

String

status
Constructor Summary

Constructors

Constructor

Description

TPTP3ProofProcessor()

***************************************************************
Method Summary

Modifier and Type

Method

Description

String

createProofDotGraph()

************************************************************* Create a proof in a format suitable for GraphViz' input format http://www.graphviz.org/.

static String

createProofDotGraphImage(String filename)

Creates a specified formatted image from a generated *.dot file from GraphViz.

Formula

extractAnswerClause(Formula ax)

*************************************************************** Return the answer clause, or null if not present

String

findTypesForSkolemTerms(KB kb)

*************************************************************** Returns the most specific type for skolem variable.

String

getInferenceType(String supportId)

***************************************************************

int

getNumFromIDtable(String id)

***************************************************************

static List<String>

getPrologArgs(String line)

*************************************************************** return the predicate and arguments to a valid prolog expression p(a1,a2...an) where a1..an are an atom, a string or a prolog expression

static boolean

isSkolemRelation(String s)

*************************************************************** Input: s__Arc13_1 Output: Arc13_1

static List<String>

joinLines(ArrayList<String> inputs)

*************************************************************** Join TPTP3 proof statements that are formatted over multiple lines.

static List<String>

joinNreverseInputLines(List<String> inputs)

*************************************************************** Join TPTP3 proof statements that are formatted over multiple lines and reverse them for Vampire, which presents proofs in reverse order.

static void

main(String[] args)

***************************************************************

List<String>

parseAnswerTuples(List<String> st, String strQuery, KB kb, StringBuilder qlist)

*************************************************************** Return a list of answers if prover finds bindings for wh- queries.

void

parseProofFromFile(String filename, KB kb)

***************************************************************

void

parseProofOutput(LineNumberReader lnr, KB kb)

*************************************************************** Compute bindings and proof from theorem prover's response

void

parseProofOutput(String st, KB kb)

***************************************************************

void

parseProofOutput(List<String> lines, String kifQuery, KB kb, StringBuilder qlist)

Parses TPTP (Thousands of Problems for Theorem Provers) proof output from a theorem prover and extracts proof steps, answer bindings, and status information.

ProofStep

parseProofStep(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).

List<Integer>

parseSupports(String supportId)

*************************************************************** Parse support / proof statements in the response

void

printAnswers()

*************************************************************** Print out prover's bindings

static void

printPrologTerm(com.igormaznitsa.prologparser.terms.PrologTerm pt)

***************************************************************

void

printProof(int level)

*************************************************************** Print proof removing some steps based on proof level 1 = full proof 2 = remove steps with single support 3 = show only axioms from the KB

void

processAnswers(String line)

*************************************************************** Return bindings from TPTP3 answer tuples

void

processAnswersFromProof(StringBuilder qlist, String query)

*************************************************************** Put bindings from TPTP3 proof answer variables into bindingMap

List<String>

removeDupInArray(List<String> input)

*************************************************************** Remove duplicates in an Array without changing the order

List<tptp_parser.TPTPFormula>

renumberProof(List<tptp_parser.TPTPFormula> proof)

*************************************************************** renumber a proof after simplification

void

renumberSupport(Map<String,tptp_parser.TPTPFormula> ftable, tptp_parser.TPTPFormula ps)

*************************************************************** Look through the chain of supporting steps for a source axiom or an axiom with more than one premise.

static List<String>

reorderVampire4_8(List<String> cleaned)

static List<String>

reorderVampireProofAnyDialect(List<String> lines)

Reorder a Vampire 4.8-style reverse proof into 5.0-style forward order.

String

replaceSkolems(String s)

*************************************************************** just replace skolem terms with "something" for now

void

setGraphFormulaFormat(TPTP3ProofProcessor.GraphFormulaFormat fmt)

static void

showHelp()

***************************************************************

List<tptp_parser.TPTPFormula>

simplifyProof(int level)

*************************************************************** Simplify proof to remove steps with single support other than axioms from the KB (plus optional readability filtering for ans*).

void

simpPara()

*************************************************************** simplify and paraphrase a proof

List<Integer>

supportIdToInts(List<String> supportIds)

*************************************************************** Parse support / proof statements in the response

static String

toFOFLine(tptp_parser.TPTPFormula f)

Format a TPTPFormula as a single fof(...) line.

String

toString()

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Details
- debug
  
  public static boolean debug
- status
  
  public String status
- noConjecture
  
  public boolean noConjecture
- inconsistency
  
  public boolean inconsistency
- containsFalse
  
  public boolean containsFalse
- bindings
  
  public List<String> bindings
- bindingMap
  
  public Map<String,String> bindingMap
- skolemTypes
  
  public Map<String,String> skolemTypes
- proof
  
  public List<tptp_parser.TPTPFormula> proof
- idTable
  
  public Map<String,Integer> idTable
Constructor Details
- TPTP3ProofProcessor
  
  public TPTP3ProofProcessor()
  
  ***************************************************************
Method Details
- toString
  
  public String toString()
  
  Overrides:
  
  toString in class Object
- joinLines
  
  public static List<String> joinLines(ArrayList<String> inputs)
  
  *************************************************************** Join TPTP3 proof statements that are formatted over multiple lines. Note that comment lines are left unchanged.
- joinNreverseInputLines
  
  public static List<String> joinNreverseInputLines(List<String> inputs)
  
  *************************************************************** Join TPTP3 proof statements that are formatted over multiple lines and reverse them for Vampire, which presents proofs in reverse order. Note that comment lines are left unchanged.
- getPrologArgs
  
  public static List<String> getPrologArgs(String line)
  
  *************************************************************** return the predicate and arguments to a valid prolog expression p(a1,a2...an) where a1..an are an atom, a string or a prolog expression
- getInferenceType
  
  public String getInferenceType(String supportId)
  
  ***************************************************************
- supportIdToInts
  
  public List<Integer> supportIdToInts(List<String> supportIds)
  
  *************************************************************** Parse support / proof statements in the response
- parseSupports
  
  public List<Integer> parseSupports(String supportId)
  
  *************************************************************** Parse support / proof statements in the response
- parseProofStep
  
  public ProofStep parseProofStep(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)invalid input: '&'~$answer(esk1_1(X1))))), inference(assume_negation,[status(cth)],[inference(add_answer_literal,[status(thm)],[c_0_0, theory(answers)])])).
- processAnswers
  
  public void processAnswers(String line)
  
  *************************************************************** Return bindings from TPTP3 answer tuples
- extractAnswerClause
  
  public Formula extractAnswerClause(Formula ax)
  
  *************************************************************** Return the answer clause, or null if not present
- removeDupInArray
  
  public List<String> removeDupInArray(List<String> input)
  
  *************************************************************** Remove duplicates in an Array without changing the order
- processAnswersFromProof
  
  public void processAnswersFromProof(StringBuilder qlist, String query)
  
  *************************************************************** Put bindings from TPTP3 proof answer variables into bindingMap
- findTypesForSkolemTerms
  
  public String findTypesForSkolemTerms(KB kb)
  
  *************************************************************** Returns the most specific type for skolem variable.
  
  Parameters:
  
  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)
  
  Returns:
  
  the most specific type for skolem variable
- isSkolemRelation
  
  public static boolean isSkolemRelation(String s)
  
  *************************************************************** Input: s__Arc13_1 Output: Arc13_1
- printAnswers
  
  public void printAnswers()
  
  *************************************************************** Print out prover's bindings
- parseProofOutput
  
  public void parseProofOutput(LineNumberReader lnr, KB kb)
  
  *************************************************************** Compute bindings and proof from theorem prover's response
- parseProofOutput
  
  public void parseProofOutput(List<String> lines, String kifQuery, KB kb, StringBuilder qlist)
  Parses TPTP (Thousands of Problems for Theorem Provers) proof output from a theorem prover and extracts proof steps, answer bindings, and status information. This method processes the textual output lines from automated theorem provers (such as Vampire or E Prover), identifying and extracting:
  
  SZS status information (e.g., "Refutation", "Theorem", "CounterSatisfiable")
  
  Answer bindings for query variables in bracketed format
  
  Individual proof steps in TPTP formula format (fof/cnf/tff)
  
  Proof metadata including support relationships and inference rules
  
  The method performs several post-processing operations:
  
  Detects potential knowledge base inconsistencies (refutations without conjectures)
  
  Strips proof step numbers from Vampire output if present
  
  Filters out type declarations in TFF proofs
  
  Normalizes proof step numbering for consistent display
  
  Extracts types for Skolem terms introduced during proving
  
  Special handling for Vampire prover: Input lines are joined and reversed before processing since Vampire presents proofs in reverse order.
  Parameters:
  
  lines - the proof output lines returned by the theorem prover
  
  kifQuery - the original query in KIF (Knowledge Interchange Format) syntax
  
  kb - the knowledge base being queried
  
  qlist - a StringBuilder containing the list of quantified variables in order, used for answer extraction and binding
  
  See Also:
  
  TPTPVisitor
  
  TPTPFormula
  
  processAnswers(String)
  
  processAnswersFromProof(StringBuilder, String)
  
  findTypesForSkolemTerms(KB)
- parseAnswerTuples
  
  public List<String> parseAnswerTuples(List<String> st, String strQuery, KB kb, StringBuilder qlist)
  
  *************************************************************** Return a list of answers if prover finds bindings for wh- queries. Return "Proof Found" if prover 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 void parseProofOutput(String st, KB kb)
  
  ***************************************************************
- parseProofFromFile
  
  public void parseProofFromFile(String filename, KB kb)
  
  ***************************************************************
- printPrologTerm
  
  public static void printPrologTerm(com.igormaznitsa.prologparser.terms.PrologTerm pt)
  
  ***************************************************************
- getNumFromIDtable
  
  public int getNumFromIDtable(String id)
  
  ***************************************************************
  
  Returns:
  
  an int from the idTable or add a new id to the table and give it a new number
- createProofDotGraphImage
  
  public static String createProofDotGraphImage(String filename) throws IOException
  
  Creates a specified formatted image from a generated *.dot file from GraphViz.
  
  Parameters:
  
  filename - the generated *.dot filename to create an image from
  
  Returns:
  
  the path to the generated image file
  
  Throws:
  
  IOException
- createProofDotGraph
  
  public String createProofDotGraph() throws IOException
  
  ************************************************************* Create a proof in a format suitable for GraphViz' input format http://www.graphviz.org/. Generate a proof imate from the .dot output with a command like dot SUMO-graph.dot -Tgif > graph.gif
  
  Throws:
  
  IOException
- setGraphFormulaFormat
  
  public void setGraphFormulaFormat(TPTP3ProofProcessor.GraphFormulaFormat fmt)
- printProof
  
  public void printProof(int level)
  
  *************************************************************** Print proof removing some steps based on proof level 1 = full proof 2 = remove steps with single support 3 = show only axioms from the KB
- renumberSupport
  
  public void renumberSupport(Map<String,tptp_parser.TPTPFormula> ftable, tptp_parser.TPTPFormula ps)
  
  *************************************************************** Look through the chain of supporting steps for a source axiom or an axiom with more than one premise.
- simplifyProof
  
  public List<tptp_parser.TPTPFormula> simplifyProof(int level)
  
  *************************************************************** Simplify proof to remove steps with single support other than axioms from the KB (plus optional readability filtering for ans*).
- renumberProof
  
  public List<tptp_parser.TPTPFormula> renumberProof(List<tptp_parser.TPTPFormula> proof)
  
  *************************************************************** renumber a proof after simplification
- reorderVampire4_8
  
  public static List<String> reorderVampire4_8(List<String> cleaned)
- reorderVampireProofAnyDialect
  
  public static List<String> reorderVampireProofAnyDialect(List<String> lines)
  
  Reorder a Vampire 4.8-style reverse proof into 5.0-style forward order. Works for FOF/TFF/THF (and CNF) blocks. Input and output are lists of lines. Expected input: ONLY the proof section lines (between SZS start/end). If you pass the whole file, non-formula lines will be preserved around the reordered blocks.
- toFOFLine
  
  public static String toFOFLine(tptp_parser.TPTPFormula f)
  
  Format a TPTPFormula as a single fof(...) line.
- replaceSkolems
  
  public String replaceSkolems(String s)
  
  *************************************************************** just replace skolem terms with "something" for now
- simpPara
  
  public void simpPara()
  
  *************************************************************** simplify and paraphrase a proof
- showHelp
  
  public static void showHelp()
  
  ***************************************************************
- main
  
  public static void main(String[] args) throws IOException
  
  ***************************************************************
  
  Throws:
  
  IOException

Class TPTP3ProofProcessor

Nested Class Summary

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Details

debug

status

noConjecture

inconsistency

containsFalse

bindings

bindingMap

skolemTypes

proof

idTable

Constructor Details

TPTP3ProofProcessor

Method Details

toString

joinLines

joinNreverseInputLines

getPrologArgs

getInferenceType

supportIdToInts

parseSupports

parseProofStep

processAnswers

extractAnswerClause

removeDupInArray

processAnswersFromProof

findTypesForSkolemTerms

isSkolemRelation

printAnswers

parseProofOutput

parseProofOutput

parseAnswerTuples

parseProofOutput

parseProofFromFile

printPrologTerm

getNumFromIDtable

createProofDotGraphImage

createProofDotGraph

setGraphFormulaFormat

printProof

renumberSupport

simplifyProof

renumberProof

reorderVampire4_8

reorderVampireProofAnyDialect

toFOFLine

replaceSkolems

simpPara

showHelp

main