Abstract
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.
| Original language | English (US) |
|---|---|
| Title of host publication | CEUR Workshop Proceedings |
| Pages | 81-93 |
| Number of pages | 13 |
| Volume | 373 |
| State | Published - 2008 |
| Event | 1st International Workshop on Practical Aspects of Automated Reasoning, PAAR 2008, Held Jointly with the Workshop on Evaluation of Systems for Higher Order Logic, ESHOL 2008 - Sydney, NSW, Australia Duration: Aug 10 2008 → Aug 11 2008 |
Other
| Other | 1st International Workshop on Practical Aspects of Automated Reasoning, PAAR 2008, Held Jointly with the Workshop on Evaluation of Systems for Higher Order Logic, ESHOL 2008 |
|---|---|
| Country | Australia |
| City | Sydney, NSW |
| Period | 8/10/08 → 8/11/08 |
Fingerprint
ASJC Scopus subject areas
- Computer Science(all)
Cite this
Presenting TSTP proofs with Inference Web tools. / Da Silva, Paolo Pinheiro; Sutcliffe, Geoffrey; Chang, Cynthia; Ding, Li; Del Rio, Nick; McGuinness, Deborah.
CEUR Workshop Proceedings. Vol. 373 2008. p. 81-93.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - Presenting TSTP proofs with Inference Web tools
AU - Da Silva, Paolo Pinheiro
AU - Sutcliffe, Geoffrey
AU - Chang, Cynthia
AU - Ding, Li
AU - Del Rio, Nick
AU - McGuinness, Deborah
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84858312799&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84858312799&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84858312799
VL - 373
SP - 81
EP - 93
BT - CEUR Workshop Proceedings
ER -