TPI Interpreters

TPII

• TPI interpreter without reasoning capability
• execute and friends can access SystemOnTPTP utility
  
• Example: Checking the axioms, asynchronously

      fof(an,axiom,p).
      fof(another,axiom,p => q).
      tpi(1,execute_async,'ASYNC_SZS_STATUS' =
          '/home/tptp/Systems/Paradox---4.0/paradox --time 300 --tstp $getgroups(tpi)').
      fof(a,conjecture,q).
      tpi(2,execute,'SZS_STATUS' =
          '/home/tptp/Systems/E---1.8/eprover --auto --cpu-limit=300 --tstp-format $getgroups(tpi)').
      tpi(3,waitenv,'ASYNC_SZS_STATUS').
      tpi(4,write,'Axioms status: ' & $getenv('ASYNC_SZS_STATUS')
           & ' Conjecture status: ' & $getenv('SZS_STATUS')).
      tpi(5,exit,exit). 

• Part of the TPTP World, and in the SystemB4TPTP interface

TPI in your Shell

• perl script to execute TPI commands from shell (script)
• Allows use of shell programming
• Slightly different syntax
• Example: Checking the axioms, asynchronously

      tpi input MyProblem.p
      tpi execute async SZS_ASYNC = 'iprover 30 $getgroups(tpi_premises)'
      tpi execute SZS = 'eprover --cpu-limit=30 --tstp-format $getgroups(tpi)'
      tpi waitenv SZS_ASYNC
      if (`tpi write '$getenv(SZS_ASYNC)'` == "Unsatisfiable") then
          set ProblemStatus = "ContradictoryAxioms"
      else
          set ProblemStatus = `tpi write '$getenv(SZS)'`
      endif
      echo "The problem status is $ProblemStatus" 

• Some funkiness with "environment variables"