This paper describes the translation of proofs in the Thousands of Solutions from Theorem Provers (TSTP) solution library to the Proof Markup Language (PML), and the subsequent use of Inference Web (IW) tools to provide new presentations of the proofs. The translation enriches the TSTP proofs with proof provenance meta-data, and provides new possibilities for proof processing.
explain, and abstract knowledge encoded in PML. In contrast to the TPTP, there is less focus on the logical data and the ne-grained reasoning processes PML supports arbitrary logical data and inference steps including, e.g., extraction of data from non-logical sources, conversion to logical forms, clausi cation and rst-order inferences, etc.
There are obvious parallels between the TPTP language/TPTPWorld and the PML language/IW toolkit. While the scope of the IW is broader than the logicfocussed TPTP/TSTP, there are obvious bene ts to building bridges between the two. Principally, the TSTP o ers a large corpora of data for testing and developing the IW, and the IW o ers alternative views of the proofs in the TSTP. This paper describes the translation of TSTP les to PML format, and the presentation of the proofs using IW tools. The contribution of this work is to add value to TPTP proofs, by translation to PML and viewing the translated proofs with IW tools. Speci c bene ts include an XML proof format for TPTP proofs, links to provenance information maintained in the IW (e.g., information about ATP systems), structural search tools (rather than greping over the text form of TPTP proofs), and new views on TPTP proofs and proof nodes.
This paper is organized as follows: Section 2 provides the necessary background about the TPTP, TSTP, and PML. Section 3 describes the translation of TSTP les into PML format. Section 4 describes four IW tools' presentations of the proofs, demonstrating the value of these di erent views. 2 2.1
The top level building blocks of TPTP and TSTP les are annotated formulae, include directives, and comments. An annotated formula has the form: language(name, role, formula, source, useful info).
The languages currently supported are fof - formulae in full rst order form,
and cnf - formulae in clause normal form. The role gives the user semantics of
the formula, e.g., axiom, definition, lemma, conjecture, which guides the use
of the formula in an ATP system. The logical formula, in either FOF or CNF,
uses a consistent and easily understood notation [
An example of an inferred CNF formula is: cnf(175,lemma, ( rsymProp(ib,sk_c3) | sk_c4 = sk_c3 ), inference(factor_simp,[status(thm)],[
inference(para_into,[status(thm)],[96,78,theory(equality)])]), [iquote('para_into,96.2.1,78.1.1,factor_simp')]).
Each problem le in the TPTP has a header section and a list of the annotated formulae that describe the problem. The header section contains information elds that provide context for the problem, including: the name and domain of the problem, short and long English descriptions of the problem, information about the source of the problem, the status of the problem in terms of the SZS ontology, and statistics about the problem. Each le in the TSTP has a header section and a list of the annotated formulae that describe the solution. The header section contains information elds that provide context for the solution, including: the name of the ATP system that produced the derivation, the name of the TPTP problem, the command line issued to run the ATP system, information about hardware and software resources used, the date and time the solution was produced, the result and output status in terms of the SZS ontology, and statistics about the solution.
At the time of writing this paper, the TPTP contains 11279 problems in 35 domains, and the TSTP contains the results of running 43 ATP systems and system variants on all the problems in the TPTP. The solution les are classi ed according to the TPTP problem domains, then by TPTP problem, and nally by the ATP systems { this information is visible in the directory hierarchy and solution le name. 2.2
PML is an interlingua for representing and sharing explanations generated by various intelligent systems such as hybrid web-based question answering systems, text analytic components, theorem provers, task processors, web services, rule engines, and machine learning components. PML is split into three modules { provenance, justi cation, and trust relations. { The provenance ontology provides primitives for recording properties of entities that have been used or processed. Properties such as name, description, date and time of creation, authors, and owner, can be recorded. The IW Registry provides a public repository that allows users to register meta-data about entities. { The justi cation ontology provides primitives for encoding justi cations for derived conclusions. Some details are provided below. { The trust relation ontology provides primitives for explaining belief assertions associated with information and trust assertions associated with sources.
PML classes are OWL [
An InferenceStep contains: { The inference rule that was applied to produce the conclusion. { The antecedent NodeSets of the inference step. { Bindings for variables in the inference. { Any number of discharged assumptions. { The original sources upon which the conclusion depends. { The inference engine that performed the inference step. { A time stamp recording when the inference step was performed.
A proof consists of a collection of NodeSets, with a root NodeSet as the nal goal, linked recursively to its antecedent NodeSets. 3
The translation of a TSTP proof into PML is done by parsing the TSTP le using the TPTP-parser4, and extracting the necessary information into PML object instances. The proof is translated into a PML NodeSet collection, with each formula in the solution being translated as singleton member of the collection (but see Section 5 for hints about future work which will aggregate proofs, so 4 A parser for the TPTP language written in Java by Andrei Tchaltsev at ITC-irst, available from http://www.freewebs.com/andrei ch/ that NodeSets may have multiple elements). Additionally, the conjecture of the corresponding TPTP problem is translated into a PML Query, and the English header eld of the problem into a PML Question. The Query contains a pointer to the Question and to all NodeSet collections (from di erent ATP systems) that provide a solution. The Query thus provides a starting point for accessing all the proofs for that problem.
To translate a TPTP formula into a PML NodeSet, the translator needs to determine the following: { The language of the formula, either fof or cnf. Both fof and cnf have corresponding PML provenance elements registered in the IW registry. { The TPTP role. This is used to help determine the inference rule of the formula. { The logical formula. The formula text is used as the NodeSet conclusion string. { The inference engine (ATP system) that produced the proof. The translator looks in the header of the TSTP le to nd the engine name. Each engine is registered in the IW registry. For example, EP has an URI of http://inference-web.org/registry/IE/EP.owl#EP. { The inference rule used to derive the formula. Leaves of proofs that have an axiom role are considered to have been derived by \direct assertion". Leaves of proofs that have an assumption role are considered to have been derived by \assumption". For internal nodes that have an inference record, the translator extracts the inference rule from the record. { The antecedent list (for inferred formulae). The members of the parent list in the inference record are used to form the antecedent list of the InferenceStep. { The external source. The source is used to form the source usage of a Node
Set's inference step to describe where the conclusion originated from. { Date and time. The translator obtains the date and time from the header of the TSTP le, to record when the proof was created.
When all information is gathered from a TSTP formula, the translator creates a NodeSet instance, and adds it to the collection forming the proof. For example, the following node from EP 0.999's proof of PUZ001+1 ... cnf(57,plain, ( hates(butler,X1) | ~ killed(X1,agatha) ), inference(spm,[status(thm)],[36,45,theory(equality)])). ... is represented by the following PML ... <rdf:RDF xmlns:pmlp="http://inference-web.org/2.0/pml-provenance.owl#" xmlns:ds="http://inference-web.org/2.0/ds.owl#" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#" xmlns:owl="http://www.w3.org/2002/07/owl#" xmlns="http://inference-web.org/2.0/pml-justification.owl#" xmlns:daml="http://www.daml.org/2001/03/daml+oil#"> <NodeSet rdf:about="http://inference-web.org/proofs/tptp/Solutions/ PUZ/PUZ001+1/EP---0.999/answer.owl#ns_57">
<pmlp:hasCreationDateTime rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime"> 2008-05-01T17:11:39-04:00</pmlp:hasCreationDateTime> <hasConclusion> <pmlp:Information>
<pmlp:hasRawString rdf:datatype="http://www.w3.org/2001/XMLSchema#string"> hates(butler,X1) | ~ killed(X1,agatha)</pmlp:hasRawString>
<pmlp:hasLanguage rdf:resource="http://inference-web.org/registry/LG/ TPTPCNF.owl#TPTPCNF"/> <pmlp:hasDescription> <pmlp:Information>
<pmlp:hasRawString rdf:datatype="http://www.w3.org/2001/XMLSchema#string"> cnf(57,plain, ( hates(butler,X1) | ~ killed(X1,agatha) ), inference(spm,[status(thm)],[36,45,theory(equality)])). </pmlp:hasRawString>
<pmlp:hasLanguage rdf:resource="http://inference-web.org/registry/LG/ TPTPCNF.owl#TPTPCNF"/>
<pmlp:hasName rdf:datatype="http://www.w3.org/2001/XMLSchema#string"> TPTP Formula</pmlp:hasName>
<pmlp:hasURL rdf:datatype="http://www.w3.org/2001/XMLSchema#anyURI"> http://www.cs.miami.edu/~tptp/cgi-bin/DVTPTP2WWW/view_file.pl?Category=Solutions& Domain=PUZ&File=PUZ001+1&System=EP---0.999.THM-CRf.s#57</pmlp:hasURL> </pmlp:Information> </pmlp:hasDescription> </pmlp:Information> </hasConclusion> <isConsequentOf> <InferenceStep> <hasIndex rdf:datatype="http://www.w3.org/2001/XMLSchema#int">0</hasIndex> <fromAnswer rdf:resource="http://inference-web.org/proofs/tptp/Solutions/PUZ/ PUZ001+1/EP---0.999/answer.owl#answer"/>
<hasInferenceRule rdf:resource="http://inference-web.org/registry/DPR/ EP0.999Spm.owl#EP0.999Spm"/> <hasAntecedentList> <NodeSetList>
<ds:first rdf:resource="http://inference-web.org/proofs/tptp/Solutions/PUZ/ PUZ001+1/EP---0.999/answer.owl#ns_36"/> <ds:rest> <NodeSetList>
<ds:first rdf:resource="http://inference-web.org/proofs/tptp/Solutions/PUZ/ PUZ001+1/EP---0.999/answer.owl#ns_45"/>
</NodeSetList> </ds:rest> </NodeSetList> </hasAntecedentList> <hasInferenceEngine rdf:resource="http://inference-web.org/registry/IE/EP.owl#EP"/> </InferenceStep> </isConsequentOf> </NodeSet> </rdf:RDF>
As an aside, the reverse translation from PML to TPTP is trivially possible
for proofs translated from TPTP to PML, because the hasConclusion element
of a NodeSet contains the original TPTP node as plain text. However,
reconstruction of the TPTP node from the other NodeSet elements is not always
completely possible because some minor items of information are not captured
in the PML form. For example, the fact that an inference used the theory of
equality, recorded by the theory(equality) parent of the TPTP node, is not
captured in the PML form. NodeSets that come from sources other than
translation from the TPTP are unlikely to be translatable to TPTP form, due to
di erent items of data being recorded, and di erent data formats being used. In
particular, the PML form records the logical formula of a proof node as a text
string in the hasConclusion element, and does not parse the formula into a
representative structure. Thus if the logical formula is in a non-TPTP language,
e.g., KIF [
Given the PML encoded proofs from the TSTP, it becomes possible to use IW tools to process the proofs. Four examples are described in this section.
The IW NodeSet browser allows the user to traverse the NodeSets of a proof. The presentation of a NodeSet provides: { the conclusion, with a control to display its metadata (which contains provenance information); { the antecedent formula and links to the NodeSets that justify (by inference) this conclusion; { links to the leaf (evidence) nodes upon which this node depends; { links to information about the ATP system and the inference rule used; { the inferred formulae and links to the NodeSets that this conclusion is used to infer, with an option to show the sibling formulae used in each case; { the formula and a link to the NodeSet nally concluded with the help of this conclusion; { the query and question answered. The Inference Web Browser (IWBrowser)5 provides a graphical rendering of a PML proof, with links to the underlying provenance information stored in the PML. The presentation also provides options to focus in on the current path to the root of the proof, and to hide nodes in the proof. Figure 3 shows an extract from EP's proof for the TPTP problem PUZ001+1, including the example from Section 4.1. The various boxed links provide the access to provenance information and rendering options. 4.3
Probe-It!6 [
IWSearch7 is a service in inference web architecture. It aims to discover, index,
and search for PML objects available on the web. IWSearch consists of three
groups of services: (i) the discovery services, which utilize Swoogle [
The translation of TSTP proofs into PML, and their presentation using IW tools, changes the strict focus on logical aspects of the proof to one that encompasses proof provenance. This type of presentation is necessary for applications that demand justi cation or explanation of the reasoning performed. This work therefore adds value to the proofs produced by ATP systems, and makes the ATP system more suitable as tools in hybrid reasoning applications.
Work on the translation of TSTP les to PML is ongoing. Improvements and new features will be made in the near future. For example, an IW tool for combining proofs will be used to aggregate proofs from di erent ATP systems proofs for a given problem. This in turn will make it possible to produce new proofs with preferred characteristics, e.g., with minimal use of certain types of reasoning. The TPTP language has recently been extended to include typed higher-order logic formulae (the \THF" format), and proofs that use this language will automatically be accomodated by the translation to PML, due to the text format used for the logic formulae.