Presenting TSTP proofs with Inference Web tools

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

Research output: Contribution to journalConference article

3 Scopus citations

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)
Pages (from-to)81-93
Number of pages13
JournalCEUR Workshop Proceedings
Volume373
StatePublished - Dec 1 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

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Presenting TSTP proofs with Inference Web tools'. Together they form a unique fingerprint.

  • 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. CEUR Workshop Proceedings, 373, 81-93.