TPTP Format for Problems

Introduction

A problem is a list of formulae. In THF, TFF, and FOF the formulae are typically any number of axioms and one conjecture. In CNF the formulae are typically any number of axioms and one or more negated conjectures.

Specifying a TPTP Format Problem

The top level building blocks of TPTP files are annotated formulae, include directives, and comments. An annotated formula has the form:
    language(name,role,formula,source,useful info).
The source and useful information are optional. The languages currently supported are thf - typed higher-order form, tff - typed first-order form, fof - (full) first-order form, and cnf - in clause normal form.

A problem is a list of annotated formulae, typically without the source or useful information. (This is a description of an ordinary problem - the TPTP language can do more than this.)

The problem files SYN000* are contrived to use most features of the TPTP language, and are thus suitable for testing parsers, etc.

Example Problem

Here is a toy FOF problem, to prove the conjecture from the axioms (not all the axioms are needed for the proof).
%------------------------------------------------------------------------ 
%----All (hu)men are created equal. John is a human. John got an F grade. 
%----There is someone (a human) who got an A grade. An A grade is not 
%----equal to an F grade. Grades are not human. Therefore there is a 
%----human other than John. 
fof(all_created_equal,axiom,( 
    ! [H1,H2] : 
      ( ( human(H1) 
         & human(H2) ) 
     => created_equal(H1,H2) ) )). 

fof(john,axiom,( 
    human(john) )). 

fof(john_failed,axiom,( 
    grade(john) = f )). 

fof(someone_got_an_a,axiom,( 
    ? [H] : 
      ( human(H) 
      & grade(H) = a ) )). 

fof(distinct_grades,axiom,( 
    a != f )). 

fof(grades_not_human,axiom,( 
    ! [G] : ~ human(grade(G)) )). 

fof(someone_not_john,conjecture,( 
    ? [H] : 
      ( human(H) 
      & H != john ) )). 
%-------------------------------------------------------------------- 

Checking a Problem

A quick way to check the syntax of a problem is to run it through tptp4X, available online in
SystemB4TPTP. Select the "Input formulae" option and paste the formulae into the text box. Select tptp4X as the system, and ensure that the output mode is System. ProcessProblem and if the syntax is faulty an error massage will be returned.

Once the syntax is OK, go to SystemOnTPTP and choose an ATP System (E is a safe bet). RunSelectedSystems and see if it solves the problem.