Presenting TSTP proofs with Inference Web tools

Paolo Pinheiro Da Silva, Geoffrey Sutcliffe, Cynthia Chang, Li Ding, Nick Del Rio, Deborah McGuinness

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

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 languageEnglish (US)
Title of host publicationCEUR Workshop Proceedings
Pages81-93
Number of pages13
Volume373
StatePublished - 2008
Event1st 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 2008Aug 11 2008

Other

Other1st 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
CountryAustralia
CitySydney, NSW
Period8/10/088/11/08

Fingerprint

Markup languages
Metadata
Processing

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

Da Silva, P. P., Sutcliffe, G., Chang, C., Ding, L., Del Rio, N., & McGuinness, D. (2008). Presenting TSTP proofs with Inference Web tools. In CEUR Workshop Proceedings (Vol. 373, pp. 81-93)

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 proceedingConference contribution

Da Silva, PP, Sutcliffe, G, Chang, C, Ding, L, Del Rio, N & McGuinness, D 2008, Presenting TSTP proofs with Inference Web tools. in CEUR Workshop Proceedings. vol. 373, pp. 81-93, 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, 8/10/08.
Da Silva PP, Sutcliffe G, Chang C, Ding L, Del Rio N, McGuinness D. Presenting TSTP proofs with Inference Web tools. In CEUR Workshop Proceedings. Vol. 373. 2008. p. 81-93
Da Silva, Paolo Pinheiro ; Sutcliffe, Geoffrey ; Chang, Cynthia ; Ding, Li ; Del Rio, Nick ; McGuinness, Deborah. / Presenting TSTP proofs with Inference Web tools. CEUR Workshop Proceedings. Vol. 373 2008. pp. 81-93
@inproceedings{b007e00bf8e640e4bcf21202d3a341cd,
title = "Presenting TSTP proofs with Inference Web tools",
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.",
author = "{Da Silva}, {Paolo Pinheiro} and Geoffrey Sutcliffe and Cynthia Chang and Li Ding and {Del Rio}, Nick and Deborah McGuinness",
year = "2008",
language = "English (US)",
volume = "373",
pages = "81--93",
booktitle = "CEUR Workshop Proceedings",

}

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 -