TPI Command Formulae

Structure

• TPTP logical formulae
    language(name,role,formula,[source[,useful info]]).
• TPI command formulae
    tpi(name,command,details,[source[,useful info]]).
• Command and logical formulae interleaved - order matters

Example, run with my_tpi_system Simple.tpi 300

    tpi(1,input,'Axioms/SET006+0.ax').
    fof(thI14,conjecture,
        ( ! [A] : equal_set(union(A,A),A) )).
    tpi(2,execute,'SZS_STATUS' =
        'eprover --auto --cpu-limit=$getargv(0) --tstp-format $getgroups(tpi)').
    tpi(3,write,'Status:' & $getenv('SZS_STATUS')).
    tpi(4,exit,exit(27)).

Implicit execute,self

• execute,self is implied at EOF if no exit
• Existing problem files are TPI files!
  Existing ATP systems are TPI systems!