TPTP World Online

• Browsing the TPTP, solving a problem, viewing a derivation
  • Browse the TPTP to the problem HAL002+1
  • "View Solutions" to that problem, and look at EP's proof
  • Go back to viewing the problem, and "Solve Problem" - that'll short-cut to the SystemOnTPTP interface with the problem name preinstalled in the "TPTP Problem" field.
  • Get a recommendation of which systems are best for this problem
  • Use SPASS to solve the problem, and get a TPTP format output.
  • Use EP to solve the problem, and view the derivation in IDV. Use the interestingness slider to generate a derivation synopsis. Try the good-bad cat button.
  • Try using the parallel mode to solve the problem. Look at the output to see which systems are recommended, which are used, and which finds a proof.
  • Cut-and-paste HAL002+1 into the "Input Formulae" box of the SystemOnTPTP interface, but delete the axioms (leaving just the include and the conjecture. Try prove it with whatever system you like - you won't succeed. Use Paradox to show that the problem is now CounterSatisfiable, i.e., not a logical consequence of the axioms (in the included axiom file).

• Preparing problems
  • Cut-and-paste HAL002+1 into the "Input Formulae" box of the SystemB4TPTP interface, and use tptp4X to check the syntax (of course it's OK). Go back, make some random syntax error, and try again.
  • Correct the problem and use the BNFParserDrill to get a feeling for the syntax, and see if you can browse through the online hyperlinked BNF to see which BNF rules are being used at each level.
  • Use FlotterOnTPTP to convert the formulae to clause normal form - are you impressed? Now use ECNF to convert the formulae to clause normal form - see any differences?
  • Run APRILS and Prophet and SInESelect on the problem. These are tools that predict which formulae are likely to be used in a proof. Compare the prediction with the axioms used by EP's proof - how accurate are they?
  • Use tptp2X to add the axioms of equality to the problem. Change the tptp2X command to tptp2X -q1 -d- -t add_equality %s to do this. How many axioms were added?
  • Cut-and-paste HAL002+1 into the "Input Formulae" box of the SystemOnTPTP interface, and add the extra axiom

    fof(subtract_to_0,axiom,
        ( element(crazy,domain)
         & subtract(domain,crazy,crazy) != zero(domain) ) ).

    It'll be real easy to prove now - you'd better check that the axioms (included and explicit) are satisfiable. Delete the conjecture and use a model finder such as Paradox or Darwin or SPASS for that, and if it fails try show them unsatisfiable using a theorem prover.

• Browsing the TSTP, verifying a solution, processing a solution
  • Browse the TSTP to EP's solution of the problem HAL002+1
  • "Process Solution" - that'll short-cut to the SystemOnTSTP interface with the problem and system names preinstalled into the "TPTP Problem" and "TSTP System" fields.
  • Verify the derivation using GDV. Shucks, seems that some steps are too hard for Otter - change the command line for GDV to GDV -p SPASS--- %s - aaah, there you go.
  • Browse the TSTP to EP's solution of the problem PUZ001-1
  • Use the Otterfier to convert all the inference steps to those of the Otter ATP system. Think why this might be useful.

• Finding problems and solutions
  • Use the TPTP2T interface to generate a list of FOF problems in the TPTP that are theorems, real first-order, have some equality, are difficult, and have been found to be theorems by the EP prover.
  • Specialize that query to require that EP solved the problem in between 5 and 20 seconds (you'll need to change to advanced mode).

• Small exercises
  • Do the exercise at the end of the notes "Using the TPTP World".
  • Do the "Osama Bin Laden" example from the notes.

Exam Style Questions