Skip to content

Format TPTP

Jump to bottom
Pascal Fontaine edited this page Nov 8, 2022 · 12 revisions

TPTP (I/O)

Short Description

Automated Theorem Proving (ATP) is an area of automated deduction that studies methods for proving and disproving conjecture formulae with respect to given axioms formulae, and for showing sets of formulae to be unsatisfiable or satisfiable. The formulae are written in some logic, including classical first-order, classical higher-order, and non-classical logics. The TPTP World is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. The TPTP language is a human-readable, easily machine-parsable, flexible, and extensible language, used for writing formulae in ATP problems and ATP solutions. The syntax is Prolog-like. The TPTP language is the de facto standard in the ATP community; most ATP systems read problems and produce solutions in the language. Problems from the TPTP Problem Library, written in the TPTP language, are used for the annual CASC competition between ATP systems.

Syntax

The top level building blocks of the TPTP language are annotated formulae. An annotated formula has the form:

    language(name,role,formula,source,useful_info).

The languages supported are clause normal form (cnf), first-order form (fof), typed first-order form (tff), and typed higher-order form (thf). The role, e.g., axiom, lemma, conjecture, defines the use of the formula in an ATP system. In the formula, terms and atoms follow Prolog conventions - functions and predicates start with a lowercase letter or are 'single quoted', and variables start with an uppercase letter. The TPTP language also supports interpreted symbols, e.g., the truth constant $true and numbers such as 27, -99.66. The basic logical connectives are !, ?, ~, |, &, =>, and <=>, for universal quantification, existential quantification, negation, disjunction, conjunction, implication, and equivalence. Equality and inequality are expressed as the infix operators = and !=. The source and useful_info are optional. An example annotated first-order formula, supplied from a file, is:

    fof(union,axiom,
        ( ! [X,A,B] :
            ( member(X,union(A,B))
          <=> ( member(X,A)
              | member(X,B) ) )
        file('SET006+0.ax',union),
        [description('Definition of union'), relevance(0.9)]).

The syntax of the TPTP languages is available in an extended BNF.

Semantics

The TPTP language provides syntax, and leaves semantics to the logic being used.

Example

An example problem in typed first-order logic is:

    tff(dog_decl,type,            dog: $tType ).
    tff(human_decl,type,          human: $tType ).
    tff(odie_decl,type,           odie: dog ).
    tff(jon_decl,type,            jon: human ).
    tff(owner_of_decl,type,       owner_of: dog > human ).
    tff(bit_decl,type,            bit: (dog * human * $int) > $o ).
    tff(hates_decl,type,          hates: (human * human) > $o ).
    
    tff(jon_owns_odie,axiom,      jon = owner_of(odie) ).
    
    tff(odie_bit_jon_twice,axiom, bit(odie,jon,2) ).
    
    tff(another_dog_bit_jon_twice,axiom,
        ? [D: dog] : ( D != odie & jon != owner_of(D) & bit(D,jon,2) ) ).
    
    tff(hate_the_multi_biter_dog,axiom,
        ! [D: dog,H: human,N: $int] :
          ( ( H != owner_of(D) & bit(D,H,N) & $greater(N,1) )
         => hates(H,owner_of(D)) ) ).
    
    tff(jon_hates_another_human,conjecture,
        ? [H: human] : ( H != jon & hates(jon,H) ) ).

A few formulae from a solution (a proof by refutation) for the problem, generated by the Vampire system, are:

    tff(dog_decl,type,            dog: $tType ).
    tff(human_decl,type,          human: $tType ).
    tff(odie_decl,type,           odie: dog ).
    tff(jon_decl,type,            jon: human ).
    tff(owner_of_decl,type,       owner_of: dog > human ).
    tff(func_def_8,type,          sK0: dog ).

%----Some formulae omitted here

tff(f3,axiom,
    ? [X0: dog] :
      ( bit(X0,jon,2) & ( jon != owner_of(X0) ) & ( odie != X0 ) ),
    file('PUZXXX-03.TF0.p',another_dog_bit_jon_twice) ).

%----Some formulae omitted here

tff(f5,conjecture,
    ? [X1: human] : ( hates(jon,X1) & ( jon != X1 ) ),
    file('PUZXXX-03.TF0.p',jon_hates_another_human) ).

tff(f6,negated_conjecture,
    ~ ? [X1: human] : ( hates(jon,X1) & ( jon != X1 ) ),
    inference(negated_conjecture,[],[f5]) ).

tff(f7,plain,
    ! [X0: dog,X1: human,X2: $int] :
      ( ( $less(1,X2) & bit(X0,X1,X2) & ( owner_of(X0) != X1 ) )
     => hates(X1,owner_of(X0)) ),
    inference(theory_normalization,[],[f4]) ).

%----Some formulae omitted here

tff(f25,plain,
    ( bit(sK0,jon,2)
    & ( jon != owner_of(sK0) )
    & ( odie != sK0 ) ),
    inference(skolemisation,[status(esa),new_symbols(skolem,[sK0])],[f3,f24]) ).

tff(f26,plain,
    ! [X0: human] :
      ( ~ hates(jon,X0) | ( jon = X0 ) ),
    inference(cnf_transformation,[],[f21]) ).

%----Some formulae omitted here

tff(f271,plain,
    ( ~ $less(1,2) | hates(jon,owner_of(sK0)) | ( jon = owner_of(sK0) ) ),
    inference(resolution,[],[f29,f32]) ).

tff(f274,plain,
    hates(jon,owner_of(sK0)),
    inference(subsumption_resolution,[],[f272,f31]) ).

tff(f276,plain,
    $false,
    inference(subsumption_resolution,[],[f275,f31]) ).

External Links

The TPTP World is available from https://www.tptp.org. Problems in the TPTP language can be browsed online. Solutions in the TPTP language can be browsed online. You can run ATP systems on TPTP problems using the SystemOnTPTP interface.

Clone this wiki locally