Cutting down the TPTP language (And others)

Nahku Saidy, Hanna Siegfried, Stephan Schulz, Geoff Sutcliffe

Research output: Contribution to journalConference articlepeer-review


Computer languages are likely to grow over time as they get more complex when their functionality is extended. An example of that is the TPTP language for automated theorem proving. Over time various forms of classical logics ranging from Clause Normal Form (CNF) to Typed Higher-order Form (THF) have been added, and that extended the TPTP language. This paper describes Synplifier, a tool that automatically extracts sub-languages from the TPTP language. Automatic extraction instead of manually maintaining sub-languages has the advantage of avoiding maintenance overhead as well as unnoticed divergences from the full language. Sub-languages of interest are for example CNF and Firstorder Form (FOF), and are extracted based on the user's selection. Synplifier has been successfully tested by extracting CNF from the TPTP language.

Original languageEnglish (US)
Pages (from-to)134-147
Number of pages14
JournalCEUR Workshop Proceedings
StatePublished - 2020
EventJoint of the 7th Workshop on Practical Aspects of Automated Reasoning and the 5th Satisfiability Checking and Symbolic Computation Workshop, PAAR+SC-Square 2020 - Virtual, Paris, France
Duration: Jul 5 2020 → …

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'Cutting down the TPTP language (And others)'. Together they form a unique fingerprint.

Cite this