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.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Paulo Pinheiro da Silva, Geoff Sutcliffe, Cynthia Chang, Li Ding, Nicholas Del Rio, Deborah L. McGuinness
• Keywords: Automated Reasoning, CADE 2008, Proof Markup Language, Proof Processing, Proof Provenance Meta-data