TPTP to PML Translation

Process

• Parse TSTP file (using Andrei Tshaltsev's Java parser)
• Extract necessary information from proof
• Extract additional information from problem comments
• Generate a singleton NodeSet collection for each node in proof

Information

• Extract information from TSTP file

• Language of formula - from principle of formula
• TPTP role - from formula
• The formula (doh!)
• Inference engine - from TSTP file header
• Inference rule - from inference() record
• Antecendents - from inference() record
• Source - the named problem file
• Date and time - from TSTP file header