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.)

Name: The name is a word starting lower case, e.g., original_f1, or a single quoted word, e.g., 'A crazy $ name'.
Role: The role is typically one of axiom for axioms, conjecture for conjectures, or negated_conjecture for negated conjectures. A full list of the posssible roles is in the TPTP syntax.
Logical formula: The logical formula uses a consistent and easily understood notation that can be seen in the BNF for THF, BNF for TFF. BNF for FOF, and BNF for CNF.

The SYN000* problem files 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 
%----another human created equal to 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) 
      & created_equal(H,john)
      & 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.